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 ) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
assume that
A5: (y `1) "\/" (x `1) = Top S and
A6: (y `1) "/\" (x `1) = Bottom S and
A7: (y `2) "\/" (x `2) = Top T and
A8: (y `2) "/\" (x `2) = Bottom T ; :: according to WAYBEL_1:def 23 :: thesis: x is_a_complement_of y
A9: (y "\/" x) `2 = (y `2) "\/" (x `2) by Th14
.= [(Top S),(Top T)] `2 by A7 ;
(y "\/" x) `1 = (y `1) "\/" (x `1) by Th14
.= [(Top S),(Top T)] `1 by A5 ;
hence y "\/" x = [(Top S),(Top T)] by A1, A9, DOMAIN_1:2
.= Top [:S,T:] by Th3 ;
:: according to WAYBEL_1:def 23 :: thesis: y "/\" x = Bottom [:S,T:]
A10: (y "/\" x) `2 = (y `2) "/\" (x `2) by Th13
.= [(Bottom S),(Bottom T)] `2 by A8 ;
(y "/\" x) `1 = (y `1) "/\" (x `1) by Th13
.= [(Bottom S),(Bottom T)] `1 by A6 ;
hence y "/\" x = [(Bottom S),(Bottom T)] by A1, A10, DOMAIN_1:2
.= Bottom [:S,T:] by Th4 ;
:: thesis: verum