begin
theorem
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem
theorem
theorem
theorem
theorem
for
S,
T being non
empty antisymmetric RelStr for
x,
y being
Element of
[:S,T:] holds
(
ex_inf_of {x,y},
[:S,T:] iff (
ex_inf_of {(x `1 ),(y `1 )},
S &
ex_inf_of {(x `2 ),(y `2 )},
T ) )
theorem
for
S,
T being non
empty antisymmetric RelStr for
x,
y being
Element of
[:S,T:] holds
(
ex_sup_of {x,y},
[:S,T:] iff (
ex_sup_of {(x `1 ),(y `1 )},
S &
ex_sup_of {(x `2 ),(y `2 )},
T ) )
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
begin
theorem Th24:
theorem
theorem
theorem
theorem Th28:
theorem
theorem
theorem
theorem
theorem Th33:
theorem
theorem
theorem
theorem Th37:
theorem
theorem
theorem
theorem Th41:
theorem
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th62:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th69:
theorem