begin
theorem Th1:
:: deftheorem defines is_in REALSET1:def 1 :
:: deftheorem Def2 defines Preserv REALSET1:def 2 :
:: deftheorem defines || REALSET1:def 3 :
theorem
canceled;
theorem Th3:
:: deftheorem Def4 defines trivial REALSET1:def 4 :
theorem Th4:
theorem
theorem Th6:
theorem
:: deftheorem defines is_Bin_Op_Preserv REALSET1:def 5 :
theorem Th8:
:: deftheorem Def6 defines Presv REALSET1:def 6 :
theorem Th9:
:: deftheorem defines ||| REALSET1:def 7 :
theorem
canceled;
:: deftheorem Def8 defines DnT REALSET1:def 8 :
theorem Th11:
:: deftheorem defines ! REALSET1:def 9 :
Lm1:
for F being non trivial set
for A being OnePoint of F ex x being Element of F st A = {x}
theorem Th12:
begin
theorem
theorem Th14:
for
A being
set holds
( not
A is
trivial iff ex
a1,
a2 being
set st
(
a1 in A &
a2 in A &
a1 <> a2 ) )
theorem
theorem
begin
theorem