let S1, S2 be non empty reflexive RelStr ; :: thesis: for D being non empty lower Subset of [:S1,S2:] holds
( proj1 D is lower & proj2 D is lower )
let D be non empty lower Subset of [:S1,S2:]; :: thesis: ( proj1 D is lower & proj2 D is lower )
set D1 = proj1 D;
set D2 = proj2 D;
the carrier of [:S1,S2:] = [:the carrier of S1,the carrier of S2:] by Def2;
then A1: D c= [:(proj1 D),(proj2 D):] by Th1;
thus proj1 D is lower :: thesis: proj2 D is lower

proof

let x, y be Element of S1; :: according to WAYBEL_0:def 19 :: thesis: ( not x in proj1 D or not y <= x or y in proj1 D )
assume A2: ( x in proj1 D & x >= y ) ; :: thesis: y in proj1 D
reconsider d2 = proj2 D as non empty Subset of S2 by Th21;
consider q1 being set such that
A3: [x,q1] in D by A2, RELAT_1:def 4;
reconsider q1 = q1 as Element of d2 by A1, A3, ZFMISC_1:106;
q1 <= q1 ;
then [x,q1] >= [y,q1] by A2, Th11;
then [y,q1] in D by A3, WAYBEL_0:def 19;
hence y in proj1 D by A1, ZFMISC_1:106; :: thesis: verum

end;

let x, y be Element of S2; :: according to WAYBEL_0:def 19 :: thesis: ( not x in proj2 D or not y <= x or y in proj2 D )
assume A4: ( x in proj2 D & x >= y ) ; :: thesis: y in proj2 D
reconsider d1 = proj1 D as non empty Subset of S1 by Th21;
consider q1 being set such that
A5: [q1,x] in D by A4, RELAT_1:def 5;
reconsider q1 = q1 as Element of d1 by A1, A5, ZFMISC_1:106;
q1 <= q1 ;
then [q1,x] >= [q1,y] by A4, Th11;
then [q1,y] in D by A5, WAYBEL_0:def 19;
hence y in proj2 D by A1, ZFMISC_1:106; :: thesis: verum