let S, T be antisymmetric bounded with_suprema with_infima RelStr ; :: thesis: for x, y being Element of [:S,T:] holds
( x is_a_complement_of y iff ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 ) )
let x, y be Element of [:S,T:]; :: thesis: ( x is_a_complement_of y iff ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 ) )

hereby :: thesis: ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 implies x is_a_complement_of y )

assume A1: x is_a_complement_of y ; :: thesis: ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 )
thus x `1 is_a_complement_of y `1 :: thesis: x `2 is_a_complement_of y `2

proof

thus (y `1 ) "\/" (x `1 ) = (y "\/" x) `1 by Th14
.= (Top [:S,T:]) `1 by A1, WAYBEL_1:def 23
.= [(Top S),(Top T)] `1 by Th3
.= Top S by MCART_1:7 ; :: according to WAYBEL_1:def 23 :: thesis: (y `1 ) "/\" (x `1 ) = Bottom S
thus (y `1 ) "/\" (x `1 ) = (y "/\" x) `1 by Th13
.= (Bottom [:S,T:]) `1 by A1, WAYBEL_1:def 23
.= [(Bottom S),(Bottom T)] `1 by Th4
.= Bottom S by MCART_1:7 ; :: thesis: verum

end;

thus x `2 is_a_complement_of y `2 :: thesis: verum

proof

thus (y `2 ) "\/" (x `2 ) = (y "\/" x) `2 by Th14
.= (Top [:S,T:]) `2 by A1, WAYBEL_1:def 23
.= [(Top S),(Top T)] `2 by Th3
.= Top T by MCART_1:7 ; :: according to WAYBEL_1:def 23 :: thesis: (y `2 ) "/\" (x `2 ) = Bottom T
thus (y `2 ) "/\" (x `2 ) = (y "/\" x) `2 by Th13
.= (Bottom [:S,T:]) `2 by A1, WAYBEL_1:def 23
.= [(Bottom S),(Bottom T)] `2 by Th4
.= Bottom T by MCART_1:7 ; :: thesis: verum

end;

end;

A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
assume that
A3: (y `1 ) "\/" (x `1 ) = Top S and
A4: (y `1 ) "/\" (x `1 ) = Bottom S and
A5: (y `2 ) "\/" (x `2 ) = Top T and
A6: (y `2 ) "/\" (x `2 ) = Bottom T ; :: according to WAYBEL_1:def 23 :: thesis: x is_a_complement_of y
A7: (y "\/" x) `1 = (y `1 ) "\/" (x `1 ) by Th14
.= [(Top S),(Top T)] `1 by A3, MCART_1:7 ;
(y "\/" x) `2 = (y `2 ) "\/" (x `2 ) by Th14
.= [(Top S),(Top T)] `2 by A5, MCART_1:7 ;
hence y "\/" x = [(Top S),(Top T)] by A2, A7, DOMAIN_1:12
.= Top [:S,T:] by Th3 ;
:: according to WAYBEL_1:def 23 :: thesis: y "/\" x = Bottom [:S,T:]
A8: (y "/\" x) `1 = (y `1 ) "/\" (x `1 ) by Th13
.= [(Bottom S),(Bottom T)] `1 by A4, MCART_1:7 ;
(y "/\" x) `2 = (y `2 ) "/\" (x `2 ) by Th13
.= [(Bottom S),(Bottom T)] `2 by A6, MCART_1:7 ;
hence y "/\" x = [(Bottom S),(Bottom T)] by A2, A8, DOMAIN_1:12
.= Bottom [:S,T:] by Th4 ;
:: thesis: verum