let S1, S2 be non empty RelStr ; :: thesis: for D being non empty Subset of [:S1,S2:] holds
( not proj1 D is empty & not proj2 D is empty )
let D be non empty Subset of [:S1,S2:]; :: thesis: ( not proj1 D is empty & not proj2 D is empty )
reconsider D1 = D as non empty Subset of [: the carrier of S1, the carrier of S2:] by Def2;
not proj1 D1 is empty ;
hence ( not proj1 D is empty & not proj2 D is empty ) ; :: thesis: verum