let S1, S2 be non empty reflexive RelStr ; :: thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds
( D1 is upper & D2 is upper )
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds
( D1 is upper & D2 is upper )
let D2 be non empty Subset of S2; :: thesis: ( [:D1,D2:] is upper implies ( D1 is upper & D2 is upper ) )
assume A1: [:D1,D2:] is upper ; :: thesis: ( D1 is upper & D2 is upper )
thus D1 is upper :: thesis: D2 is upper

proof

let x, y be Element of S1; :: according to WAYBEL_0:def 20 :: thesis: ( not x in D1 or not x <= y or y in D1 )
assume A2: ( x in D1 & x <= y ) ; :: thesis: y in D1
consider q1 being Element of D2;
A3: [x,q1] in [:D1,D2:] by A2, ZFMISC_1:106;
q1 <= q1 ;
then [x,q1] <= [y,q1] by A2, Th11;
then [y,q1] in [:D1,D2:] by A1, A3, WAYBEL_0:def 20;
hence y in D1 by ZFMISC_1:106; :: thesis: verum

end;

let x, y be Element of S2; :: according to WAYBEL_0:def 20 :: thesis: ( not x in D2 or not x <= y or y in D2 )
assume A4: ( x in D2 & x <= y ) ; :: thesis: y in D2
consider q1 being Element of D1;
A5: [q1,x] in [:D1,D2:] by A4, ZFMISC_1:106;
q1 <= q1 ;
then [q1,x] <= [q1,y] by A4, Th11;
then [q1,y] in [:D1,D2:] by A1, A5, WAYBEL_0:def 20;
hence y in D2 by ZFMISC_1:106; :: thesis: verum