let L be RelStr ; :: thesis: for X being Subset of L
for Y being Subset of (L opp ) st X = Y holds
( downarrow X = uparrow Y & uparrow X = downarrow Y )
let X be Subset of L; :: thesis: for Y being Subset of (L opp ) st X = Y holds
( downarrow X = uparrow Y & uparrow X = downarrow Y )
let Y be Subset of (L opp ); :: thesis: ( X = Y implies ( downarrow X = uparrow Y & uparrow X = downarrow Y ) )
assume A1: X = Y ; :: thesis: ( downarrow X = uparrow Y & uparrow X = downarrow Y )
thus downarrow X c= uparrow Y :: according to XBOOLE_0:def 10 :: thesis: ( uparrow Y c= downarrow X & uparrow X = downarrow Y )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow X or x in uparrow Y )
assume A2: x in downarrow X ; :: thesis: x in uparrow Y
then reconsider x = x as Element of L ;
consider y being Element of L such that
A3: ( y >= x & y in X ) by A2, WAYBEL_0:def 15;
( y ~ <= x ~ & y ~ = y & x ~ = x ) by A3, LATTICE3:9;
hence x in uparrow Y by A1, A3, WAYBEL_0:def 16; :: thesis: verum

end;

thus uparrow Y c= downarrow X :: thesis: uparrow X = downarrow Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow Y or x in downarrow X )
assume A4: x in uparrow Y ; :: thesis: x in downarrow X
then reconsider x = x as Element of (L opp ) ;
consider y being Element of (L opp ) such that
A5: ( y <= x & y in Y ) by A4, WAYBEL_0:def 16;
( ~ y >= ~ x & ~ y = y & ~ x = x ) by A5, Th1;
hence x in downarrow X by A1, A5, WAYBEL_0:def 15; :: thesis: verum

end;

thus uparrow X c= downarrow Y :: according to XBOOLE_0:def 10 :: thesis: downarrow Y c= uparrow X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow X or x in downarrow Y )
assume A6: x in uparrow X ; :: thesis: x in downarrow Y
then reconsider x = x as Element of L ;
consider y being Element of L such that
A7: ( y <= x & y in X ) by A6, WAYBEL_0:def 16;
( y ~ >= x ~ & y ~ = y & x ~ = x ) by A7, LATTICE3:9;
hence x in downarrow Y by A1, A7, WAYBEL_0:def 15; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow Y or x in uparrow X )
assume A8: x in downarrow Y ; :: thesis: x in uparrow X
then reconsider x = x as Element of (L opp ) ;
consider y being Element of (L opp ) such that
A9: ( y >= x & y in Y ) by A8, WAYBEL_0:def 15;
( ~ y <= ~ x & ~ y = y & ~ x = x ) by A9, Th1;
hence x in uparrow X by A1, A9, WAYBEL_0:def 16; :: thesis: verum