let T be non empty 1-sorted ; :: thesis: for V, W being Subset of T
for S being TopAugmentation of BoolePoset {0}
for f, g being Function of T,S st f = chi (V, the carrier of T) & g = chi (W, the carrier of T) holds
( V c= W iff f <= g )
let V, W be Subset of T; :: thesis: for S being TopAugmentation of BoolePoset {0}
for f, g being Function of T,S st f = chi (V, the carrier of T) & g = chi (W, the carrier of T) holds
( V c= W iff f <= g )
let S be TopAugmentation of BoolePoset {0}; :: thesis: for f, g being Function of T,S st f = chi (V, the carrier of T) & g = chi (W, the carrier of T) holds
( V c= W iff f <= g )
let c1, c2 be Function of T,S; :: thesis: ( c1 = chi (V, the carrier of T) & c2 = chi (W, the carrier of T) implies ( V c= W iff c1 <= c2 ) )
assume that
A1: c1 = chi (V, the carrier of T) and
A2: c2 = chi (W, the carrier of T) ; :: thesis: ( V c= W iff c1 <= c2 )
A3: RelStr(# the carrier of S, the InternalRel of S #) = BoolePoset {0} by YELLOW_9:def 4;
hereby :: thesis: ( c1 <= c2 implies V c= W )
assume A4: V c= W ; :: thesis: c1 <= c2
now :: thesis: for z being set st z in the carrier of T holds
ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b )
let z be set ; :: thesis: ( z in the carrier of T implies ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b ) )
assume z in the carrier of T ; :: thesis: ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b )
then reconsider x = z as Element of T ;
reconsider a = c1 . x, b = c2 . x as Element of (BoolePoset {0}) by A3;
( ( x in V & x in W ) or not x in V ) by A4;
then ( ( c1 . x = 1 & c2 . x = 1 ) or c1 . x = 0 ) by A1, A2, FUNCT_3:def 3;
then c1 . x c= c2 . x ;
then a <= b by YELLOW_1:2;
hence ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b ) by A3, YELLOW_0:1; :: thesis: verum
end;
hence c1 <= c2 ; :: thesis: verum
end;
assume A5: c1 <= c2 ; :: thesis: V c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V or x in W )
assume that
A6: x in V and
A7: not x in W ; :: thesis: contradiction
reconsider x = x as Element of T by A6;
A8: c2 . x = 0 by A2, A7, FUNCT_3:def 3;
A9: 0 c= {0} ;
reconsider a = c1 . x, b = c2 . x as Element of (BoolePoset {0}) by A3;
ex a, b being Element of S st
( a = c1 . x & b = c2 . x & a <= b ) by A5;
then A10: a <= b by A3, YELLOW_0:1;
c1 . x = 1 by A1, A6, FUNCT_3:def 3;
then {0} c= 0 by A8, A10, YELLOW_1:2, CARD_1:49;
hence contradiction by A9, XBOOLE_0:def 10; :: thesis: verum