NAT_LAT

:: NAT_LAT semantic presentation

begin

definition

func hcflat -> ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) means :: NAT_LAT:def 1
for m, n being ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) holds it : ( ( ) ( ) LattStr ) . (m : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) ,n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) ) : ( ( ) ( ) set ) = m : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) gcd n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

func lcmlat -> ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) means :: NAT_LAT:def 2
for m, n being ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) holds it : ( ( ) ( ) LattStr ) . (m : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) ,n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) ) : ( ( ) ( ) set ) = m : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) lcm n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

end;

definition

func Nat_Lattice -> ( ( non empty strict ) ( non empty strict ) LattStr ) equals :: NAT_LAT:def 3
LattStr(# NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ,hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) #) : ( ( strict ) ( non empty strict ) LattStr ) ;

end;

registration

cluster the carrier of Nat_Lattice : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) -> natural-membered ;

end;

registration

let p, q be ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ;

end;

theorem :: NAT_LAT:1

for p, q being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) "\/" q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of the carrier of Nat_Lattice : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) = p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) lcm q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: NAT_LAT:2

for p, q being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) "/\" q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of the carrier of Nat_Lattice : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) = p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) gcd q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: NAT_LAT:3

for a, b being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) st a : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) [= b : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds
a : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) divides b : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ;

definition

func 0_NN -> ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) equals :: NAT_LAT:def 4
1 : ( ( ) ( non empty ext-real positive epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

func 1_NN -> ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) equals :: NAT_LAT:def 5
0 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

end;

theorem :: NAT_LAT:4

0_NN : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) = 1 : ( ( ) ( non empty ext-real positive epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

registration

cluster Nat_Lattice : ( ( non empty strict ) ( non empty strict ) LattStr ) -> non empty strict Lattice-like ;

end;

registration

cluster Nat_Lattice : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -> non empty strict ;

end;

registration

cluster Nat_Lattice : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -> non empty strict lower-bounded ;

end;

theorem :: NAT_LAT:5

for p, q being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) = lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: NAT_LAT:6

for q, p being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) = hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: NAT_LAT:7

for p, q, r being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: NAT_LAT:8

for p, q, r being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds
( lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) & lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) & lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) & lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: NAT_LAT:9

for p, q, r being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: NAT_LAT:10

for p, q, r being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds
( hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) & hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) & hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) & hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (r : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: NAT_LAT:11

for q, p being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds
( hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) & hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) & hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) & hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) ;

theorem :: NAT_LAT:12

for q, p being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) holds
( lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) & lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) & lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,(hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) & lcmlat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . ((hcflat : ( ( Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) ( Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) -valued Function-like V18([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ) BinOp of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) . (q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ,p : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) )) : ( ( ) ( ) set ) ,q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) : ( ( ) ( ) set ) = q : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) ) ;

definition

func NATPLUS -> ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) means :: NAT_LAT:def 6
for n being ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) holds
( n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) in it : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) iff 0 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) < n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) );

end;

registration

cluster NATPLUS : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) -> non empty ;

end;

definition

let D be ( ( non empty ) ( non empty ) set ) ;
let S be ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) ;
let N be ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) ;
:: original: Element
redefine mode Element of N -> ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ;

end;

registration

let D be ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( ) set ) ) ;

cluster -> real for ( ( ) ( ) Element of D : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) ;

end;

registration

let D be ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ;

cluster -> real for ( ( ) ( ) Element of D : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) ;

end;

definition

mode NatPlus is ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ;

end;

definition

let k be ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) ;
assume k : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Nat) > 0 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

func @ k -> ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) equals :: NAT_LAT:def 7
k : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ;

end;

registration

cluster -> non zero natural for ( ( ) ( ) Element of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ;

end;

definition

func hcflatplus -> ( ( Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like [:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) BinOp of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) means :: NAT_LAT:def 8
for m, n being ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) holds it : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) . (m : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) ,n : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) = m : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) gcd n : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

func lcmlatplus -> ( ( Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like [:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) BinOp of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) means :: NAT_LAT:def 9
for m, n being ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) holds it : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) . (m : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) ,n : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) Element of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) = m : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) lcm n : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

end;

definition

func NatPlus_Lattice -> ( ( strict ) ( strict ) LattStr ) equals :: NAT_LAT:def 10
LattStr(# NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,lcmlatplus : ( ( Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like [:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) BinOp of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ,hcflatplus : ( ( Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like [:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like V18([:NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ,NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) ) BinOp of NATPLUS : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Subset of ( ( ) ( ) set ) ) ) #) : ( ( strict ) ( non empty strict ) LattStr ) ;

end;

registration

cluster NatPlus_Lattice : ( ( strict ) ( strict ) LattStr ) -> non empty strict ;

end;

definition

let m be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

func @ m -> ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) equals :: NAT_LAT:def 11
m : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ;

end;

registration

cluster -> non zero natural for ( ( ) ( ) Element of the carrier of NatPlus_Lattice : ( ( strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

let p, q be ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) ;

end;

theorem :: NAT_LAT:13

for p, q being ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) holds p : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of the carrier of NatPlus_Lattice : ( ( strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) = (@ p : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) lcm (@ q : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: NAT_LAT:14

for p, q being ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) holds p : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of the carrier of NatPlus_Lattice : ( ( strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) = (@ p : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) gcd (@ q : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non zero ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() ) NatPlus) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V49() ) set ) : ( ( ) ( ) set ) ) ) ;

registration

cluster NatPlus_Lattice : ( ( strict ) ( non empty strict ) LattStr ) -> strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing ;

end;

definition

let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;

mode SubLattice of L -> ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) means :: NAT_LAT:def 12
( the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) c= the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) & the L_join of it : ( ( non empty ) ( non empty ) set ) : ( ( Function-like V18([: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = the L_join of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( Function-like V18([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) || the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & the L_meet of it : ( ( non empty ) ( non empty ) set ) : ( ( Function-like V18([: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = the L_meet of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( Function-like V18([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) || the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) );

end;

registration

let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for ( ( ) ( ) SubLattice of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) ;

end;

theorem :: NAT_LAT:15

for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) holds L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: NAT_LAT:16