let T be non empty 1-sorted ; 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; 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}; 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; ( 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)
; ( V c= W iff c1 <= c2 )
A3:
RelStr(# the carrier of S, the InternalRel of S #) = BoolePoset {0}
by YELLOW_9:def 4;
hereby ( c1 <= c2 implies V c= W )
assume A4:
V c= W
;
c1 <= c2hence
c1 <= c2
;
verum
end;
assume A5:
c1 <= c2
; V c= W
let x be object ; TARSKI:def 3 ( not x in V or x in W )
assume that
A6:
x in V
and
A7:
not x in W
; 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; verum