let S1, S2 be non empty reflexive RelStr ; for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )
let D1 be non empty Subset of S1; for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )
let D2 be non empty Subset of S2; ( [:D1,D2:] is lower implies ( D1 is lower & D2 is lower ) )
assume A1:
[:D1,D2:] is lower
; ( D1 is lower & D2 is lower )
thus
D1 is lower
D2 is lower proof
set q1 = the
Element of
D2;
let x,
y be
Element of
S1;
WAYBEL_0:def 19 ( not x in D1 or not y <= x or y in D1 )
assume that A2:
x in D1
and A3:
x >= y
;
y in D1
A4:
[x, the Element of D2] in [:D1,D2:]
by A2, ZFMISC_1:87;
the
Element of
D2 <= the
Element of
D2
;
then
[x, the Element of D2] >= [y, the Element of D2]
by A3, Th11;
then
[y, the Element of D2] in [:D1,D2:]
by A1, A4;
hence
y in D1
by ZFMISC_1:87;
verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; WAYBEL_0:def 19 ( not x in D2 or not y <= x or y in D2 )
assume that
A5:
x in D2
and
A6:
x >= y
; y in D2
A7:
[ the Element of D1,x] in [:D1,D2:]
by A5, ZFMISC_1:87;
the Element of D1 <= the Element of D1
;
then
[ the Element of D1,x] >= [ the Element of D1,y]
by A6, Th11;
then
[ the Element of D1,y] in [:D1,D2:]
by A1, A7;
hence
y in D2
by ZFMISC_1:87; verum