let S1, S2 be non empty reflexive RelStr ; :: thesis: for D being non empty filtered Subset of [:S1,S2:] holds
( proj1 D is filtered & proj2 D is filtered )
let D be non empty filtered Subset of [:S1,S2:]; :: thesis: ( proj1 D is filtered & proj2 D is filtered )
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 filtered
:: thesis: proj2 D is filtered proof
let x,
y be
Element of
S1;
:: according to WAYBEL_0:def 2 :: thesis: ( not x in proj1 D or not y in proj1 D or ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & b1 <= x & b1 <= y ) )
assume A2:
(
x in proj1 D &
y in proj1 D )
;
:: thesis: ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & b1 <= x & b1 <= y )
then reconsider D1' =
proj1 D as non
empty Subset of
S1 ;
reconsider D2' =
proj2 D as non
empty Subset of
S2 by A2, FUNCT_5:19;
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 A3, RELAT_1:def 5;
consider q2 being
set such that A4:
[y,q2] in D
by A2, RELAT_1:def 4;
reconsider q2 =
q2 as
Element of
D2' by A4, RELAT_1:def 5;
consider z being
Element of
[:S1,S2:] such that A5:
(
z in D &
[x,q1] >= z &
[y,q2] >= z )
by A3, A4, WAYBEL_0:def 2;
reconsider zz =
z `1 as
Element of
D1' by A1, A5, MCART_1:10;
reconsider z2 =
z `2 as
Element of
D2' by A1, A5, MCART_1:10;
take
zz
;
:: thesis: ( zz in proj1 D & zz <= x & zz <= y )
thus
zz in proj1 D
;
:: thesis: ( zz <= x & zz <= y )
ex
x,
y being
set st
(
x in D1' &
y in D2' &
z = [x,y] )
by A1, A5, ZFMISC_1:def 2;
then
z = [zz,z2]
by MCART_1:8;
hence
(
zz <= x &
zz <= y )
by A5, Th11;
:: thesis: verum
end;
let x, y be Element of S2; :: according to WAYBEL_0:def 2 :: thesis: ( not x in proj2 D or not y in proj2 D or ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & b1 <= x & b1 <= y ) )
assume A6:
( x in proj2 D & y in proj2 D )
; :: thesis: ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & b1 <= x & b1 <= y )
then reconsider D1' = proj1 D as non empty Subset of S1 by FUNCT_5:19;
reconsider D2' = proj2 D as non empty Subset of S2 by A6;
consider q1 being set such that
A7:
[q1,x] in D
by A6, RELAT_1:def 5;
reconsider q1 = q1 as Element of D1' by A7, RELAT_1:def 4;
consider q2 being set such that
A8:
[q2,y] in D
by A6, RELAT_1:def 5;
reconsider q2 = q2 as Element of D1' by A8, RELAT_1:def 4;
consider z being Element of [:S1,S2:] such that
A9:
( z in D & [q1,x] >= z & [q2,y] >= z )
by A7, A8, WAYBEL_0:def 2;
reconsider zz = z `2 as Element of D2' by A1, A9, MCART_1:10;
reconsider z2 = z `1 as Element of D1' by A1, A9, MCART_1:10;
take
zz
; :: thesis: ( zz in proj2 D & zz <= x & zz <= y )
thus
zz in proj2 D
; :: thesis: ( zz <= x & zz <= y )
ex x, y being set st
( x in D1' & y in D2' & z = [x,y] )
by A1, A9, ZFMISC_1:def 2;
then
z = [z2,zz]
by MCART_1:8;
hence
( zz <= x & zz <= y )
by A9, Th11; :: thesis: verum