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 object ; :: 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 and
A4: y in X by A2, WAYBEL_0:def 15;
y ~ <= x ~ by A3, LATTICE3:9;
hence x in uparrow Y by A1, A4, WAYBEL_0:def 16; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow Y or x in downarrow X )
assume A5: 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
A6: y <= x and
A7: y in Y by A5, WAYBEL_0:def 16;
~ y >= ~ x by A6, Th1;
hence x in downarrow X by A1, A7, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow X or x in downarrow Y )
assume A8: 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
A9: y <= x and
A10: y in X by A8, WAYBEL_0:def 16;
y ~ >= x ~ by A9, LATTICE3:9;
hence x in downarrow Y by A1, A10, WAYBEL_0:def 15; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow Y or x in uparrow X )
assume A11: 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
A12: y >= x and
A13: y in Y by A11, WAYBEL_0:def 15;
~ y <= ~ x by A12, Th1;
hence x in uparrow X by A1, A13, WAYBEL_0:def 16; :: thesis: verum