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 )

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

thus
downarrow Y c= downarrow X
:: thesis: uparrow X = uparrow Y
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;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

proof

thus
uparrow X c= uparrow Y
:: according to XBOOLE_0:def 10 :: thesis: uparrow Y c= uparrow X
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;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

proof

thus
uparrow Y c= uparrow X
:: thesis: verum
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;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

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;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