let T be non empty 1-sorted ; :: thesis: for V, W being Subset of T
for S being TopAugmentation of BoolePoset 1
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 1
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 1; :: 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 1 by YELLOW_9:def 4;

hereby :: thesis: ( c1 <= c2 implies V c= W )

assume A4: V c= W ; :: thesis: c1 <= c2

now

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 1) 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 by XBOOLE_1:2;
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 by YELLOW_2:def 1; :: thesis: verum

end;

assume A5: c1 <= c2 ; :: thesis: V c= W
let x be set ; :: 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= 1 by XBOOLE_1:2;
reconsider a = c1 . x, b = c2 . x as Element of (BoolePoset 1) by A3;
ex a, b being Element of S st
( a = c1 . x & b = c2 . x & a <= b ) by A5, YELLOW_2:def 1;
then A10: a <= b by A3, YELLOW_0:1;
c1 . x = 1 by A1, A6, FUNCT_3:def 3;
then 1 c= 0 by A8, A10, YELLOW_1:2;
hence contradiction by A9, XBOOLE_0:def 10; :: thesis: verum