:: REALSET1 semantic presentation

theorem Th1: :: REALSET1:1
for b1, b2 being set
for b3 being Function of [:b1,b1:],b1 st b2 in [:b1,b1:] holds
b3 . b2 in b1
proof end;

theorem Th2: :: REALSET1:2
for b1 being set
for b2 being BinOp of b1 ex b3 being Subset of b1 st
for b4 being set st b4 in [:b3,b3:] holds
b2 . b4 in b3
proof end;

definition
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Subset of c1;
pred c2 is_in c3 means :: REALSET1:def 1
for b1 being set st b1 in [:a3,a3:] holds
a2 . b1 in a3;
end;

:: deftheorem Def1 defines is_in REALSET1:def 1 :
for b1 being set
for b2 being BinOp of b1
for b3 being Subset of b1 holds
( b2 is_in b3 iff for b4 being set st b4 in [:b3,b3:] holds
b2 . b4 in b3 );

definition
let c1 be set ;
let c2 be BinOp of c1;
mode Preserv of c2 -> Subset of a1 means :Def2: :: REALSET1:def 2
for b1 being set st b1 in [:a3,a3:] holds
a2 . b1 in a3;
existence
ex b1 being Subset of c1 st
for b2 being set st b2 in [:b1,b1:] holds
c2 . b2 in b1 by Th2;
end;

:: deftheorem Def2 defines Preserv REALSET1:def 2 :
for b1 being set
for b2 being BinOp of b1
for b3 being Subset of b1 holds
( b3 is Preserv of b2 iff for b4 being set st b4 in [:b3,b3:] holds
b2 . b4 in b3 );

definition
let c1 be Relation;
let c2 be set ;
func c1 || c2 -> set equals :: REALSET1:def 3
a1 | [:a2,a2:];
coherence
c1 | [:c2,c2:] is set ;
end;

:: deftheorem Def3 defines || REALSET1:def 3 :
for b1 being Relation
for b2 being set holds b1 || b2 = b1 | [:b2,b2:];

registration
let c1 be Relation;
let c2 be set ;
cluster a1 || a2 -> Relation-like ;
coherence
c1 || c2 is Relation-like ;
end;

registration
let c1 be Function;
let c2 be set ;
cluster a1 || a2 -> Relation-like Function-like ;
coherence
c1 || c2 is Function-like ;
end;

theorem Th3: :: REALSET1:3
for b1 being set
for b2 being BinOp of b1
for b3 being Preserv of b2 holds b2 || b3 is BinOp of b3
proof end;

definition
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Preserv of c2;
redefine func || as c2 || c3 -> BinOp of a3;
coherence
c2 || c3 is BinOp of c3 by Th3;
end;

definition
let c1 be set ;
attr a1 is trivial means :Def4: :: REALSET1:def 4
( a1 is empty or ex b1 being set st a1 = {b1} );
end;

:: deftheorem Def4 defines trivial REALSET1:def 4 :
for b1 being set holds
( b1 is trivial iff ( b1 is empty or ex b2 being set st b1 = {b2} ) );

registration
cluster non empty trivial set ;
existence
ex b1 being set st
( b1 is trivial & not b1 is empty )
proof end;
cluster non empty non trivial set ;
existence
ex b1 being set st
( not b1 is trivial & not b1 is empty )
proof end;
cluster non trivial -> non empty set ;
coherence
for b1 being set st not b1 is trivial holds
not b1 is empty
proof end;
end;

registration
let c1 be set ;
cluster {a1} -> trivial ;
coherence
{c1} is trivial by Def4;
end;

theorem Th4: :: REALSET1:4
for b1 being non empty set holds
( not b1 is trivial iff for b2 being set holds b1 \ {b2} is non empty set )
proof end;

theorem Th5: :: REALSET1:5
ex b1 being non empty set st
for b2 being Element of b1 holds b1 \ {b2} is non empty set
proof end;

theorem Th6: :: REALSET1:6
for b1 being non empty set st ( for b2 being Element of b1 holds b1 \ {b2} is non empty set ) holds
not b1 is trivial
proof end;

theorem Th7: :: REALSET1:7
for b1 being non empty set st ( for b2 being Element of b1 holds b1 \ {b2} is non empty set ) holds
b1 is non trivial set by Th6;

definition
let c1 be non trivial set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
pred c2 is_Bin_Op_Preserv c3 means :: REALSET1:def 5
( a1 \ {a3} is Preserv of a2 & (a2 || a1) \ {a3} is BinOp of a1 \ {a3} );
correctness
;
end;

:: deftheorem Def5 defines is_Bin_Op_Preserv REALSET1:def 5 :
for b1 being non trivial set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b2 is_Bin_Op_Preserv b3 iff ( b1 \ {b3} is Preserv of b2 & (b2 || b1) \ {b3} is BinOp of b1 \ {b3} ) );

theorem Th8: :: REALSET1:8
for b1 being set
for b2 being Subset of b1 ex b3 being BinOp of b1 st
for b4 being set st b4 in [:b2,b2:] holds
b3 . b4 in b2
proof end;

definition
let c1 be set ;
let c2 be Subset of c1;
mode Presv of c1,c2 -> BinOp of a1 means :Def6: :: REALSET1:def 6
for b1 being set st b1 in [:a2,a2:] holds
a3 . b1 in a2;
existence
ex b1 being BinOp of c1 st
for b2 being set st b2 in [:c2,c2:] holds
b1 . b2 in c2 by Th8;
end;

:: deftheorem Def6 defines Presv REALSET1:def 6 :
for b1 being set
for b2 being Subset of b1
for b3 being BinOp of b1 holds
( b3 is Presv of b1,b2 iff for b4 being set st b4 in [:b2,b2:] holds
b3 . b4 in b2 );

theorem Th9: :: REALSET1:9
for b1 being set
for b2 being Subset of b1
for b3 being Presv of b1,b2 holds b3 || b2 is BinOp of b2
proof end;

definition
let c1 be set ;
let c2 be Subset of c1;
let c3 be Presv of c1,c2;
func c3 ||| c2 -> BinOp of a2 equals :: REALSET1:def 7
a3 || a2;
coherence
c3 || c2 is BinOp of c2 by Th9;
end;

:: deftheorem Def7 defines ||| REALSET1:def 7 :
for b1 being set
for b2 being Subset of b1
for b3 being Presv of b1,b2 holds b3 ||| b2 = b3 || b2;

theorem Th10: :: REALSET1:10
for b1 being set
for b2 being Element of b1 ex b3 being BinOp of b1 st
for b4 being set st b4 in [:(b1 \ {b2}),(b1 \ {b2}):] holds
b3 . b4 in b1 \ {b2}
proof end;

definition
let c1 be set ;
let c2 be Element of c1;
mode DnT of c2,c1 -> BinOp of a1 means :Def8: :: REALSET1:def 8
for b1 being set st b1 in [:(a1 \ {a2}),(a1 \ {a2}):] holds
a3 . b1 in a1 \ {a2};
existence
ex b1 being BinOp of c1 st
for b2 being set st b2 in [:(c1 \ {c2}),(c1 \ {c2}):] holds
b1 . b2 in c1 \ {c2} by Th10;
end;

:: deftheorem Def8 defines DnT REALSET1:def 8 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b3 is DnT of b2,b1 iff for b4 being set st b4 in [:(b1 \ {b2}),(b1 \ {b2}):] holds
b3 . b4 in b1 \ {b2} );

theorem Th11: :: REALSET1:11
for b1 being non trivial set
for b2 being Element of b1
for b3 being DnT of b2,b1 holds b3 || (b1 \ {b2}) is BinOp of b1 \ {b2}
proof end;

definition
let c1 be non trivial set ;
let c2 be Element of c1;
let c3 be DnT of c2,c1;
func c3 ! c1,c2 -> BinOp of a1 \ {a2} equals :: REALSET1:def 9
a3 || (a1 \ {a2});
coherence
c3 || (c1 \ {c2}) is BinOp of c1 \ {c2} by Th11;
end;

:: deftheorem Def9 defines ! REALSET1:def 9 :
for b1 being non trivial set
for b2 being Element of b1
for b3 being DnT of b2,b1 holds b3 ! b1,b2 = b3 || (b1 \ {b2});

definition
let c1 be non trivial set ;
mode OnePoint of c1 -> set means :Def10: :: REALSET1:def 10
ex b1 being Element of a1 st a2 = {b1};
existence
ex b1 being set ex b2 being Element of c1 st b1 = {b2}
proof end;
end;

:: deftheorem Def10 defines OnePoint REALSET1:def 10 :
for b1 being non trivial set
for b2 being set holds
( b2 is OnePoint of b1 iff ex b3 being Element of b1 st b2 = {b3} );

theorem Th12: :: REALSET1:12
for b1 being non trivial set
for b2 being OnePoint of b1 holds b1 \ b2 is non empty set
proof end;

registration
let c1 be non trivial set ;
let c2 be OnePoint of c1;
cluster a1 \ a2 -> non empty ;
coherence
not c1 \ c2 is empty by Th12;
end;

registration
let c1 be non trivial set ;
cluster non empty OnePoint of a1;
existence
not for b1 being OnePoint of c1 holds b1 is empty
proof end;
end;

definition
let c1 be non trivial set ;
let c2 be Element of c1;
redefine func { as {c2} -> OnePoint of a1;
coherence
{c2} is OnePoint of c1 by Def10;
end;

theorem Th13: :: REALSET1:13
for b1 being finite set holds
( b1 is trivial iff card b1 < 2 )
proof end;

theorem Th14: :: REALSET1:14
for b1 being set holds
( not b1 is trivial iff ex b2, b3 being set st
( b2 in b1 & b3 in b1 & b2 <> b3 ) )
proof end;

theorem Th15: :: REALSET1:15
for b1 being set
for b2 being Subset of b1 holds
( not b2 is trivial iff ex b3, b4 being Element of b1 st
( b3 in b2 & b4 in b2 & b3 <> b4 ) )
proof end;