begin
theorem Th1:
:: deftheorem Def2 defines Preserv REALSET1:def 1 :
for X being set
for F being BinOp of X
for b3 being Subset of X holds
( b3 is Preserv of F iff for x being set st x in [:b3,b3:] holds
F . x in b3 );
:: deftheorem defines || REALSET1:def 2 :
for R being Relation
for A being set holds R || A = R | [:A,A:];
theorem Th3:
theorem Th4:
theorem
:: deftheorem defines is_Bin_Op_Preserv REALSET1:def 3 :
for X being non trivial set
for F being BinOp of X
for x being Element of X holds
( F is_Bin_Op_Preserv x iff ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ) );
theorem Th8:
:: deftheorem Def6 defines Presv REALSET1:def 4 :
for X being set
for A being Subset of X
for b3 being BinOp of X holds
( b3 is Presv of X,A iff for x being set st x in [:A,A:] holds
b3 . x in A );
theorem Th9:
:: deftheorem defines ||| REALSET1:def 5 :
for X being set
for A being Subset of X
for F being Presv of X,A holds F ||| A = F || A;
:: deftheorem Def8 defines DnT REALSET1:def 6 :
for A being set
for x being Element of A
for b3 being BinOp of A holds
( b3 is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b3 . y in A \ {x} );
theorem Th11:
:: deftheorem defines ! REALSET1:def 7 :
for A being non trivial set
for x being Element of A
for F being DnT of x,A holds F ! (A,x) = F || (A \ {x});
theorem Th12: