:: Group and Field Definitions
:: by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: REALSET1:1
:: deftheorem defines is_in REALSET1:def 1 :
:: deftheorem Def2 defines Preserv REALSET1:def 2 :
:: deftheorem defines || REALSET1:def 3 :
theorem :: REALSET1:2
canceled;
theorem Th3: :: REALSET1:3
:: deftheorem Def4 defines trivial REALSET1:def 4 :
theorem Th4: :: REALSET1:4
theorem :: REALSET1:5
theorem Th6: :: REALSET1:6
theorem :: REALSET1:7
:: deftheorem defines is_Bin_Op_Preserv REALSET1:def 5 :
theorem Th8: :: REALSET1:8
:: deftheorem Def6 defines Presv REALSET1:def 6 :
theorem Th9: :: REALSET1:9
:: deftheorem defines ||| REALSET1:def 7 :
theorem :: REALSET1:10
canceled;
:: deftheorem Def8 defines DnT REALSET1:def 8 :
theorem Th11: :: REALSET1:11
:: 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: :: REALSET1:12
theorem :: REALSET1:13
theorem Th14: :: REALSET1:14
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 :: REALSET1:15
theorem :: REALSET1:16
theorem :: REALSET1:17