let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y ) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
let X be Subset of L1; :: thesis: for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
let Y be Subset of L2; :: thesis: ( X = Y implies ( downarrow X = downarrow Y & uparrow X = uparrow Y ) )
assume A2: X = Y ; :: thesis: ( downarrow X = downarrow Y & uparrow X = uparrow Y )
thus downarrow X c= downarrow Y :: according to XBOOLE_0:def 10 :: thesis: ( downarrow Y c= downarrow X & uparrow X = uparrow Y )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow X or x in downarrow Y )
assume A3: x in downarrow X ; :: thesis: x in downarrow Y
then reconsider x = x as Element of L1 ;
reconsider x9 = x as Element of L2 by A1;
consider y being Element of L1 such that
A4: y >= x and
A5: y in X by A3, Def15;
reconsider y9 = y as Element of L2 by A1;
y9 >= x9 by A1, A4, YELLOW_0:1;
hence x in downarrow Y by A2, A5, Def15; :: thesis: verum
end;
thus downarrow Y c= downarrow X :: thesis: uparrow X = uparrow Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow Y or x in downarrow X )
assume A6: x in downarrow Y ; :: thesis: x in downarrow X
then reconsider x = x as Element of L2 ;
reconsider x9 = x as Element of L1 by A1;
consider y being Element of L2 such that
A7: y >= x and
A8: y in Y by A6, Def15;
reconsider y9 = y as Element of L1 by A1;
y9 >= x9 by A1, A7, YELLOW_0:1;
hence x in downarrow X by A2, A8, Def15; :: thesis: verum
end;
thus uparrow X c= uparrow Y :: according to XBOOLE_0:def 10 :: thesis: uparrow Y c= uparrow X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow X or x in uparrow Y )
assume A9: x in uparrow X ; :: thesis: x in uparrow Y
then reconsider x = x as Element of L1 ;
reconsider x9 = x as Element of L2 by A1;
consider y being Element of L1 such that
A10: y <= x and
A11: y in X by A9, Def16;
reconsider y9 = y as Element of L2 by A1;
y9 <= x9 by A1, A10, YELLOW_0:1;
hence x in uparrow Y by A2, A11, Def16; :: thesis: verum
end;
thus uparrow Y c= uparrow X :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow Y or x in uparrow X )
assume A12: x in uparrow Y ; :: thesis: x in uparrow X
then reconsider x = x as Element of L2 ;
reconsider x9 = x as Element of L1 by A1;
consider y being Element of L2 such that
A13: y <= x and
A14: y in Y by A12, Def16;
reconsider y9 = y as Element of L1 by A1;
y9 <= x9 by A1, A13, YELLOW_0:1;
hence x in uparrow X by A2, A14, Def16; :: thesis: verum
end;