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 )
A1: RelStr(# the carrier of S,the InternalRel of S #) = BoolePoset 1 by YELLOW_9:def 4;
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 A2: ( c1 = chi V,the carrier of T & c2 = chi W,the carrier of T ) ; :: thesis: ( V c= W iff c1 <= c2 )

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

assume A3: 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 A1;
( ( x in V & x in W ) or not x in V ) by A3;
then ( ( c1 . x = 1 & c2 . x = 1 ) or c1 . x = 0 ) by A2, FUNCT_3:def 3;
then c1 . x c= c2 . x by XBOOLE_1:2;
then a <= b by YELLOW_1:2;
then c1 . x <= c2 . x by A1, YELLOW_0:1;
hence ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b ) ; :: thesis: verum

end;

hence c1 <= c2 by YELLOW_2:def 1; :: thesis: verum

end;

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