set cn = the carrier of M_3;

let L be LATTICE; :: thesis: ( ex K being full Sublattice of L st M_3 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) )

A1: the carrier of M_3 = {0,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;

thus ( ex K being full Sublattice of L st M_3 ,K are_isomorphic implies ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) ) :: thesis: ( ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) implies ex K being full Sublattice of L st M_3 ,K are_isomorphic )

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) implies ex K being full Sublattice of L st M_3 ,K are_isomorphic ) :: thesis: verum

let L be LATTICE; :: thesis: ( ex K being full Sublattice of L st M_3 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) )

A1: the carrier of M_3 = {0,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;

thus ( ex K being full Sublattice of L st M_3 ,K are_isomorphic implies ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) ) :: thesis: ( ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) implies ex K being full Sublattice of L st M_3 ,K are_isomorphic )

proof

thus
( ex a, b, c, d, e being Element of L st
reconsider td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider dj = 2 \ 1 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider j = 1 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider cl = the carrier of L as non empty set ;

reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;

given K being full Sublattice of L such that A2: M_3 ,K are_isomorphic ; :: thesis: ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e )

consider f being Function of M_3,K such that

A3: f is isomorphic by A2;

A4: not K is empty by A3, WAYBEL_0:def 38;

then A5: ( f is one-to-one & f is monotone ) by A3, WAYBEL_0:def 38;

reconsider K = K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;

reconsider ck = the carrier of K as non empty set ;

A6: ck = rng f by A3, WAYBEL_0:66;

reconsider g = f as Function of the carrier of M_3,ck ;

reconsider a = g . z, b = g . j, c = g . dj, d = g . td, e = g . t as Element of K ;

reconsider ck = ck as non empty Subset of cl by YELLOW_0:def 13;

A7: b in ck ;

A8: c in ck ;

A9: e in ck ;

A10: d in ck ;

a in ck ;

then reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;

take A ; :: thesis: ex b, c, d, e being Element of L st

( A,b,c,d,e are_mutually_distinct & A "/\" b = A & A "/\" c = A & A "/\" d = A & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = A & b "/\" d = A & c "/\" d = A & b "\/" c = e & b "\/" d = e & c "\/" d = e )

take B ; :: thesis: ex c, d, e being Element of L st

( A,B,c,d,e are_mutually_distinct & A "/\" B = A & A "/\" c = A & A "/\" d = A & B "/\" e = B & c "/\" e = c & d "/\" e = d & B "/\" c = A & B "/\" d = A & c "/\" d = A & B "\/" c = e & B "\/" d = e & c "\/" d = e )

take C ; :: thesis: ex d, e being Element of L st

( A,B,C,d,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & A "/\" d = A & B "/\" e = B & C "/\" e = C & d "/\" e = d & B "/\" C = A & B "/\" d = A & C "/\" d = A & B "\/" C = e & B "\/" d = e & C "\/" d = e )

take D ; :: thesis: ex e being Element of L st

( A,B,C,D,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" e = B & C "/\" e = C & D "/\" e = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = e & B "\/" D = e & C "\/" D = e )

take E ; :: thesis: ( A,B,C,D,E are_mutually_distinct & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> B by A5, WAYBEL_1:def 1; :: according to ZFMISC_1:def 7 :: thesis: ( not A = C & not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> C by A5, Th2, WAYBEL_1:def 1; :: thesis: ( not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> D by A5, Th4, WAYBEL_1:def 1; :: thesis: ( not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> E by A5, WAYBEL_1:def 1; :: thesis: ( not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus B <> E by A5, WAYBEL_1:def 1; :: thesis: ( not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

z c= j ;

then z <= j by YELLOW_1:3;

then a <= b by A3, WAYBEL_0:66;

then A <= B by YELLOW_0:59;

hence A "/\" B = A by YELLOW_0:25; :: thesis: ( A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

z c= dj ;

then z <= dj by YELLOW_1:3;

then a <= c by A3, WAYBEL_0:66;

then A <= C by YELLOW_0:59;

hence A "/\" C = A by YELLOW_0:25; :: thesis: ( A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

z c= td ;

then z <= td by YELLOW_1:3;

then a <= d by A3, WAYBEL_0:66;

then A <= D by YELLOW_0:59;

hence A "/\" D = A by YELLOW_0:25; :: thesis: ( B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

Segm 1 c= Segm 3 by NAT_1:39;

then j <= t by YELLOW_1:3;

then b <= e by A3, WAYBEL_0:66;

then B <= E by YELLOW_0:59;

hence B "/\" E = B by YELLOW_0:25; :: thesis: ( C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

dj c= t

then c <= e by A3, WAYBEL_0:66;

then C <= E by YELLOW_0:59;

hence C "/\" E = C by YELLOW_0:25; :: thesis: ( D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

td <= t by YELLOW_1:3;

then d <= e by A3, WAYBEL_0:66;

then D <= E by YELLOW_0:59;

hence D "/\" E = D by YELLOW_0:25; :: thesis: ( B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus B "/\" C = A :: thesis: ( B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

end;reconsider dj = 2 \ 1 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider j = 1 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider cl = the carrier of L as non empty set ;

reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;

given K being full Sublattice of L such that A2: M_3 ,K are_isomorphic ; :: thesis: ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e )

consider f being Function of M_3,K such that

A3: f is isomorphic by A2;

A4: not K is empty by A3, WAYBEL_0:def 38;

then A5: ( f is one-to-one & f is monotone ) by A3, WAYBEL_0:def 38;

reconsider K = K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;

reconsider ck = the carrier of K as non empty set ;

A6: ck = rng f by A3, WAYBEL_0:66;

reconsider g = f as Function of the carrier of M_3,ck ;

reconsider a = g . z, b = g . j, c = g . dj, d = g . td, e = g . t as Element of K ;

reconsider ck = ck as non empty Subset of cl by YELLOW_0:def 13;

A7: b in ck ;

A8: c in ck ;

A9: e in ck ;

A10: d in ck ;

a in ck ;

then reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;

take A ; :: thesis: ex b, c, d, e being Element of L st

( A,b,c,d,e are_mutually_distinct & A "/\" b = A & A "/\" c = A & A "/\" d = A & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = A & b "/\" d = A & c "/\" d = A & b "\/" c = e & b "\/" d = e & c "\/" d = e )

take B ; :: thesis: ex c, d, e being Element of L st

( A,B,c,d,e are_mutually_distinct & A "/\" B = A & A "/\" c = A & A "/\" d = A & B "/\" e = B & c "/\" e = c & d "/\" e = d & B "/\" c = A & B "/\" d = A & c "/\" d = A & B "\/" c = e & B "\/" d = e & c "\/" d = e )

take C ; :: thesis: ex d, e being Element of L st

( A,B,C,d,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & A "/\" d = A & B "/\" e = B & C "/\" e = C & d "/\" e = d & B "/\" C = A & B "/\" d = A & C "/\" d = A & B "\/" C = e & B "\/" d = e & C "\/" d = e )

take D ; :: thesis: ex e being Element of L st

( A,B,C,D,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" e = B & C "/\" e = C & D "/\" e = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = e & B "\/" D = e & C "\/" D = e )

take E ; :: thesis: ( A,B,C,D,E are_mutually_distinct & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> B by A5, WAYBEL_1:def 1; :: according to ZFMISC_1:def 7 :: thesis: ( not A = C & not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> C by A5, Th2, WAYBEL_1:def 1; :: thesis: ( not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> D by A5, Th4, WAYBEL_1:def 1; :: thesis: ( not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus A <> E by A5, WAYBEL_1:def 1; :: thesis: ( not B = C & not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

now :: thesis: not f . j = f . dj

hence
B <> C
; :: thesis: ( not B = D & not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )assume
f . j = f . dj
; :: thesis: contradiction

then j = dj by A4, A5, WAYBEL_1:def 1;

then 1 in 1 by Th2, TARSKI:def 1;

hence contradiction ; :: thesis: verum

end;then j = dj by A4, A5, WAYBEL_1:def 1;

then 1 in 1 by Th2, TARSKI:def 1;

hence contradiction ; :: thesis: verum

now :: thesis: not f . j = f . td

hence
B <> D
; :: thesis: ( not B = E & not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )assume
f . j = f . td
; :: thesis: contradiction

then A11: j = td by A4, A5, WAYBEL_1:def 1;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A11, Th4, TARSKI:def 1; :: thesis: verum

end;then A11: j = td by A4, A5, WAYBEL_1:def 1;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A11, Th4, TARSKI:def 1; :: thesis: verum

thus B <> E by A5, WAYBEL_1:def 1; :: thesis: ( not C = D & not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

now :: thesis: not f . dj = f . td

hence
C <> D
; :: thesis: ( not C = E & not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )assume
f . dj = f . td
; :: thesis: contradiction

then A12: dj = td by A4, A5, WAYBEL_1:def 1;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A12, Th4, TARSKI:def 1; :: thesis: verum

end;then A12: dj = td by A4, A5, WAYBEL_1:def 1;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A12, Th4, TARSKI:def 1; :: thesis: verum

now :: thesis: not f . dj = f . t

hence
C <> E
; :: thesis: ( not D = E & A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )assume
f . dj = f . t
; :: thesis: contradiction

then A13: dj = t by A4, A5, WAYBEL_1:def 1;

0 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A13, Th2, TARSKI:def 1; :: thesis: verum

end;then A13: dj = t by A4, A5, WAYBEL_1:def 1;

0 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A13, Th2, TARSKI:def 1; :: thesis: verum

now :: thesis: not f . td = f . t

hence
D <> E
; :: thesis: ( A "/\" B = A & A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )assume
f . td = f . t
; :: thesis: contradiction

then A14: td = t by A4, A5, WAYBEL_1:def 1;

0 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A14, Th4, TARSKI:def 1; :: thesis: verum

end;then A14: td = t by A4, A5, WAYBEL_1:def 1;

0 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A14, Th4, TARSKI:def 1; :: thesis: verum

z c= j ;

then z <= j by YELLOW_1:3;

then a <= b by A3, WAYBEL_0:66;

then A <= B by YELLOW_0:59;

hence A "/\" B = A by YELLOW_0:25; :: thesis: ( A "/\" C = A & A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

z c= dj ;

then z <= dj by YELLOW_1:3;

then a <= c by A3, WAYBEL_0:66;

then A <= C by YELLOW_0:59;

hence A "/\" C = A by YELLOW_0:25; :: thesis: ( A "/\" D = A & B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

z c= td ;

then z <= td by YELLOW_1:3;

then a <= d by A3, WAYBEL_0:66;

then A <= D by YELLOW_0:59;

hence A "/\" D = A by YELLOW_0:25; :: thesis: ( B "/\" E = B & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

Segm 1 c= Segm 3 by NAT_1:39;

then j <= t by YELLOW_1:3;

then b <= e by A3, WAYBEL_0:66;

then B <= E by YELLOW_0:59;

hence B "/\" E = B by YELLOW_0:25; :: thesis: ( C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

dj c= t

proof

then
dj <= t
by YELLOW_1:3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dj or x in t )

assume x in dj ; :: thesis: x in t

then x = 1 by Th2, TARSKI:def 1;

hence x in t by CARD_1:51, ENUMSET1:def 1; :: thesis: verum

end;assume x in dj ; :: thesis: x in t

then x = 1 by Th2, TARSKI:def 1;

hence x in t by CARD_1:51, ENUMSET1:def 1; :: thesis: verum

then c <= e by A3, WAYBEL_0:66;

then C <= E by YELLOW_0:59;

hence C "/\" E = C by YELLOW_0:25; :: thesis: ( D "/\" E = D & B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

td <= t by YELLOW_1:3;

then d <= e by A3, WAYBEL_0:66;

then D <= E by YELLOW_0:59;

hence D "/\" E = D by YELLOW_0:25; :: thesis: ( B "/\" C = A & B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

thus B "/\" C = A :: thesis: ( B "/\" D = A & C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )

proof

then inf {B,C} in the carrier of K by YELLOW_0:def 16;

then B "/\" C in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 3;

hence B "/\" C = A by A1, A17, A21, A15, A19, ENUMSET1:def 3; :: thesis: verum

end;

thus
B "/\" D = A
:: thesis: ( C "/\" D = A & B "\/" C = E & B "\/" D = E & C "\/" D = E )A15: now :: thesis: not B "/\" C = D

assume
B "/\" C = D
; :: thesis: contradiction

then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then td <= dj by A3, WAYBEL_0:66;

then A16: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A16, Th2, TARSKI:def 1; :: thesis: verum

end;then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then td <= dj by A3, WAYBEL_0:66;

then A16: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A16, Th2, TARSKI:def 1; :: thesis: verum

A17: now :: thesis: not B "/\" C = B

assume
B "/\" C = B
; :: thesis: contradiction

then B <= C by YELLOW_0:25;

then b <= c by YELLOW_0:60;

then j <= dj by A3, WAYBEL_0:66;

then A18: j c= dj by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A18, Th2, TARSKI:def 1; :: thesis: verum

end;then B <= C by YELLOW_0:25;

then b <= c by YELLOW_0:60;

then j <= dj by A3, WAYBEL_0:66;

then A18: j c= dj by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A18, Th2, TARSKI:def 1; :: thesis: verum

A19: now :: thesis: not B "/\" C = E

assume
B "/\" C = E
; :: thesis: contradiction

then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dj by A3, WAYBEL_0:66;

then A20: t c= dj by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A20, Th2, TARSKI:def 1; :: thesis: verum

end;then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dj by A3, WAYBEL_0:66;

then A20: t c= dj by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A20, Th2, TARSKI:def 1; :: thesis: verum

A21: now :: thesis: not B "/\" C = C

ex_inf_of {B,C},L
by YELLOW_0:21;assume
B "/\" C = C
; :: thesis: contradiction

then C <= B by YELLOW_0:25;

then c <= b by YELLOW_0:60;

then dj <= j by A3, WAYBEL_0:66;

then A22: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A22, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;then C <= B by YELLOW_0:25;

then c <= b by YELLOW_0:60;

then dj <= j by A3, WAYBEL_0:66;

then A22: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A22, CARD_1:49, TARSKI:def 1; :: thesis: verum

then inf {B,C} in the carrier of K by YELLOW_0:def 16;

then B "/\" C in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 3;

hence B "/\" C = A by A1, A17, A21, A15, A19, ENUMSET1:def 3; :: thesis: verum

proof

then inf {B,D} in the carrier of K by YELLOW_0:def 16;

then B "/\" D in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & B "/\" D = f . x ) by FUNCT_1:def 3;

hence B "/\" D = A by A1, A27, A25, A23, A29, ENUMSET1:def 3; :: thesis: verum

end;

thus
C "/\" D = A
:: thesis: ( B "\/" C = E & B "\/" D = E & C "\/" D = E )A23: now :: thesis: not B "/\" D = D

assume
B "/\" D = D
; :: thesis: contradiction

then D <= B by YELLOW_0:23;

then d <= b by YELLOW_0:60;

then td <= j by A3, WAYBEL_0:66;

then A24: td c= j by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A24, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;then D <= B by YELLOW_0:23;

then d <= b by YELLOW_0:60;

then td <= j by A3, WAYBEL_0:66;

then A24: td c= j by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A24, CARD_1:49, TARSKI:def 1; :: thesis: verum

A25: now :: thesis: not B "/\" D = C

assume
B "/\" D = C
; :: thesis: contradiction

then C <= B by YELLOW_0:23;

then c <= b by YELLOW_0:60;

then dj <= j by A3, WAYBEL_0:66;

then A26: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A26, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;then C <= B by YELLOW_0:23;

then c <= b by YELLOW_0:60;

then dj <= j by A3, WAYBEL_0:66;

then A26: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A26, CARD_1:49, TARSKI:def 1; :: thesis: verum

A27: now :: thesis: not B "/\" D = B

assume
B "/\" D = B
; :: thesis: contradiction

then B <= D by YELLOW_0:25;

then b <= d by YELLOW_0:60;

then j <= td by A3, WAYBEL_0:66;

then A28: j c= td by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A28, Th4, TARSKI:def 1; :: thesis: verum

end;then B <= D by YELLOW_0:25;

then b <= d by YELLOW_0:60;

then j <= td by A3, WAYBEL_0:66;

then A28: j c= td by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A28, Th4, TARSKI:def 1; :: thesis: verum

A29: now :: thesis: not B "/\" D = E

ex_inf_of {B,D},L
by YELLOW_0:21;assume
B "/\" D = E
; :: thesis: contradiction

then E <= B by YELLOW_0:23;

then e <= b by YELLOW_0:60;

then t <= j by A3, WAYBEL_0:66;

then A30: t c= j by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A30, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;then E <= B by YELLOW_0:23;

then e <= b by YELLOW_0:60;

then t <= j by A3, WAYBEL_0:66;

then A30: t c= j by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A30, CARD_1:49, TARSKI:def 1; :: thesis: verum

then inf {B,D} in the carrier of K by YELLOW_0:def 16;

then B "/\" D in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & B "/\" D = f . x ) by FUNCT_1:def 3;

hence B "/\" D = A by A1, A27, A25, A23, A29, ENUMSET1:def 3; :: thesis: verum

proof

then inf {C,D} in the carrier of K by YELLOW_0:def 16;

then C "/\" D in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 3;

hence C "/\" D = A by A1, A37, A35, A31, A33, ENUMSET1:def 3; :: thesis: verum

end;

thus
B "\/" C = E
:: thesis: ( B "\/" D = E & C "\/" D = E )A31: now :: thesis: not C "/\" D = D

assume
C "/\" D = D
; :: thesis: contradiction

then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then td <= dj by A3, WAYBEL_0:66;

then A32: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A32, Th2, TARSKI:def 1; :: thesis: verum

end;then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then td <= dj by A3, WAYBEL_0:66;

then A32: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A32, Th2, TARSKI:def 1; :: thesis: verum

A33: now :: thesis: not C "/\" D = E

assume
C "/\" D = E
; :: thesis: contradiction

then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dj by A3, WAYBEL_0:66;

then A34: t c= dj by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A34, Th2, TARSKI:def 1; :: thesis: verum

end;then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dj by A3, WAYBEL_0:66;

then A34: t c= dj by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A34, Th2, TARSKI:def 1; :: thesis: verum

A35: now :: thesis: not C "/\" D = C

assume
C "/\" D = C
; :: thesis: contradiction

then C <= D by YELLOW_0:25;

then c <= d by YELLOW_0:60;

then dj <= td by A3, WAYBEL_0:66;

then A36: dj c= td by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A36, Th4, TARSKI:def 1; :: thesis: verum

end;then C <= D by YELLOW_0:25;

then c <= d by YELLOW_0:60;

then dj <= td by A3, WAYBEL_0:66;

then A36: dj c= td by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A36, Th4, TARSKI:def 1; :: thesis: verum

A37: now :: thesis: not C "/\" D = B

ex_inf_of {C,D},L
by YELLOW_0:21;assume
C "/\" D = B
; :: thesis: contradiction

then B <= C by YELLOW_0:23;

then b <= c by YELLOW_0:60;

then j <= dj by A3, WAYBEL_0:66;

then A38: j c= dj by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A38, Th2, TARSKI:def 1; :: thesis: verum

end;then B <= C by YELLOW_0:23;

then b <= c by YELLOW_0:60;

then j <= dj by A3, WAYBEL_0:66;

then A38: j c= dj by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A38, Th2, TARSKI:def 1; :: thesis: verum

then inf {C,D} in the carrier of K by YELLOW_0:def 16;

then C "/\" D in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 3;

hence C "/\" D = A by A1, A37, A35, A31, A33, ENUMSET1:def 3; :: thesis: verum

proof

then sup {B,C} in the carrier of K by YELLOW_0:def 17;

then B "\/" C in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 3;

hence B "\/" C = E by A1, A41, A39, A43, A45, ENUMSET1:def 3; :: thesis: verum

end;

thus
B "\/" D = E
:: thesis: C "\/" D = EA39: now :: thesis: not B "\/" C = C

assume
B "\/" C = C
; :: thesis: contradiction

then C >= B by YELLOW_0:24;

then c >= b by YELLOW_0:60;

then dj >= j by A3, WAYBEL_0:66;

then A40: j c= dj by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A40, Th2, TARSKI:def 1; :: thesis: verum

end;then C >= B by YELLOW_0:24;

then c >= b by YELLOW_0:60;

then dj >= j by A3, WAYBEL_0:66;

then A40: j c= dj by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A40, Th2, TARSKI:def 1; :: thesis: verum

A41: now :: thesis: not B "\/" C = B

assume
B "\/" C = B
; :: thesis: contradiction

then B >= C by YELLOW_0:24;

then b >= c by YELLOW_0:60;

then j >= dj by A3, WAYBEL_0:66;

then A42: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A42, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;then B >= C by YELLOW_0:24;

then b >= c by YELLOW_0:60;

then j >= dj by A3, WAYBEL_0:66;

then A42: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A42, CARD_1:49, TARSKI:def 1; :: thesis: verum

A43: now :: thesis: not B "\/" C = D

assume
B "\/" C = D
; :: thesis: contradiction

then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then td >= dj by A3, WAYBEL_0:66;

then A44: dj c= td by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A44, Th4, TARSKI:def 1; :: thesis: verum

end;then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then td >= dj by A3, WAYBEL_0:66;

then A44: dj c= td by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A44, Th4, TARSKI:def 1; :: thesis: verum

A45: now :: thesis: not B "\/" C = A

ex_sup_of {B,C},L
by YELLOW_0:20;assume
B "\/" C = A
; :: thesis: contradiction

then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dj by A3, WAYBEL_0:66;

then dj c= z by YELLOW_1:3;

hence contradiction by Th2; :: thesis: verum

end;then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dj by A3, WAYBEL_0:66;

then dj c= z by YELLOW_1:3;

hence contradiction by Th2; :: thesis: verum

then sup {B,C} in the carrier of K by YELLOW_0:def 17;

then B "\/" C in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 3;

hence B "\/" C = E by A1, A41, A39, A43, A45, ENUMSET1:def 3; :: thesis: verum

proof

then sup {B,D} in the carrier of K by YELLOW_0:def 17;

then B "\/" D in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & B "\/" D = f . x ) by FUNCT_1:def 3;

hence B "\/" D = E by A1, A48, A50, A46, A52, ENUMSET1:def 3; :: thesis: verum

end;

thus
C "\/" D = E
:: thesis: verumA46: now :: thesis: not B "\/" D = D

assume
B "\/" D = D
; :: thesis: contradiction

then D >= B by YELLOW_0:22;

then d >= b by YELLOW_0:60;

then td >= j by A3, WAYBEL_0:66;

then A47: j c= td by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A47, Th4, TARSKI:def 1; :: thesis: verum

end;then D >= B by YELLOW_0:22;

then d >= b by YELLOW_0:60;

then td >= j by A3, WAYBEL_0:66;

then A47: j c= td by YELLOW_1:3;

0 in j by CARD_1:49, TARSKI:def 1;

hence contradiction by A47, Th4, TARSKI:def 1; :: thesis: verum

A48: now :: thesis: not B "\/" D = B

assume
B "\/" D = B
; :: thesis: contradiction

then B >= D by YELLOW_0:22;

then b >= d by YELLOW_0:60;

then j >= td by A3, WAYBEL_0:66;

then A49: td c= j by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A49, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;then B >= D by YELLOW_0:22;

then b >= d by YELLOW_0:60;

then j >= td by A3, WAYBEL_0:66;

then A49: td c= j by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A49, CARD_1:49, TARSKI:def 1; :: thesis: verum

A50: now :: thesis: not B "\/" D = C

assume
B "\/" D = C
; :: thesis: contradiction

then C >= D by YELLOW_0:22;

then c >= d by YELLOW_0:60;

then dj >= td by A3, WAYBEL_0:66;

then A51: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A51, Th2, TARSKI:def 1; :: thesis: verum

end;then C >= D by YELLOW_0:22;

then c >= d by YELLOW_0:60;

then dj >= td by A3, WAYBEL_0:66;

then A51: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A51, Th2, TARSKI:def 1; :: thesis: verum

A52: now :: thesis: not B "\/" D = A

ex_sup_of {B,D},L
by YELLOW_0:20;assume
B "\/" D = A
; :: thesis: contradiction

then A >= B by YELLOW_0:22;

then a >= b by YELLOW_0:60;

then z >= j by A3, WAYBEL_0:66;

then j c= z by YELLOW_1:3;

hence contradiction ; :: thesis: verum

end;then A >= B by YELLOW_0:22;

then a >= b by YELLOW_0:60;

then z >= j by A3, WAYBEL_0:66;

then j c= z by YELLOW_1:3;

hence contradiction ; :: thesis: verum

then sup {B,D} in the carrier of K by YELLOW_0:def 17;

then B "\/" D in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & B "\/" D = f . x ) by FUNCT_1:def 3;

hence B "\/" D = E by A1, A48, A50, A46, A52, ENUMSET1:def 3; :: thesis: verum

proof

then sup {C,D} in the carrier of K by YELLOW_0:def 17;

then C "\/" D in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 3;

hence C "\/" D = E by A1, A53, A57, A55, A59, ENUMSET1:def 3; :: thesis: verum

end;

A53: now :: thesis: not C "\/" D = B

assume
C "\/" D = B
; :: thesis: contradiction

then B >= C by YELLOW_0:22;

then b >= c by YELLOW_0:60;

then j >= dj by A3, WAYBEL_0:66;

then A54: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

then 1 in 1 by A54;

hence contradiction ; :: thesis: verum

end;then B >= C by YELLOW_0:22;

then b >= c by YELLOW_0:60;

then j >= dj by A3, WAYBEL_0:66;

then A54: dj c= j by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

then 1 in 1 by A54;

hence contradiction ; :: thesis: verum

A55: now :: thesis: not C "\/" D = D

assume
C "\/" D = D
; :: thesis: contradiction

then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then td >= dj by A3, WAYBEL_0:66;

then A56: dj c= td by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A56, Th4, TARSKI:def 1; :: thesis: verum

end;then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then td >= dj by A3, WAYBEL_0:66;

then A56: dj c= td by YELLOW_1:3;

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A56, Th4, TARSKI:def 1; :: thesis: verum

A57: now :: thesis: not C "\/" D = C

assume
C "\/" D = C
; :: thesis: contradiction

then C >= D by YELLOW_0:24;

then c >= d by YELLOW_0:60;

then dj >= td by A3, WAYBEL_0:66;

then A58: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A58, Th2, TARSKI:def 1; :: thesis: verum

end;then C >= D by YELLOW_0:24;

then c >= d by YELLOW_0:60;

then dj >= td by A3, WAYBEL_0:66;

then A58: td c= dj by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A58, Th2, TARSKI:def 1; :: thesis: verum

A59: now :: thesis: not C "\/" D = A

ex_sup_of {C,D},L
by YELLOW_0:20;assume
C "\/" D = A
; :: thesis: contradiction

then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dj by A3, WAYBEL_0:66;

then dj c= z by YELLOW_1:3;

hence contradiction by Th2; :: thesis: verum

end;then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dj by A3, WAYBEL_0:66;

then dj c= z by YELLOW_1:3;

hence contradiction by Th2; :: thesis: verum

then sup {C,D} in the carrier of K by YELLOW_0:def 17;

then C "\/" D in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 3;

hence C "\/" D = E by A1, A53, A57, A55, A59, ENUMSET1:def 3; :: thesis: verum

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) implies ex K being full Sublattice of L st M_3 ,K are_isomorphic ) :: thesis: verum

proof

given a, b, c, d, e being Element of L such that AAA:
a,b,c,d,e are_mutually_distinct
and

A70: a "/\" b = a and

A71: a "/\" c = a and

A72: a "/\" d = a and

A73: b "/\" e = b and

A74: c "/\" e = c and

A75: d "/\" e = d and

A76: b "/\" c = a and

A77: b "/\" d = a and

A78: c "/\" d = a and

A79: b "\/" c = e and

A80: b "\/" d = e and

A81: c "\/" d = e ; :: thesis: ex K being full Sublattice of L st M_3 ,K are_isomorphic

set ck = {a,b,c,d,e};

reconsider ck = {a,b,c,d,e} as Subset of L ;

set K = subrelstr ck;

A82: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;

A83: subrelstr ck is meet-inheriting

take K ; :: thesis: M_3 ,K are_isomorphic

thus M_3 ,K are_isomorphic :: thesis: verum

end;A70: a "/\" b = a and

A71: a "/\" c = a and

A72: a "/\" d = a and

A73: b "/\" e = b and

A74: c "/\" e = c and

A75: d "/\" e = d and

A76: b "/\" c = a and

A77: b "/\" d = a and

A78: c "/\" d = a and

A79: b "\/" c = e and

A80: b "\/" d = e and

A81: c "\/" d = e ; :: thesis: ex K being full Sublattice of L st M_3 ,K are_isomorphic

set ck = {a,b,c,d,e};

reconsider ck = {a,b,c,d,e} as Subset of L ;

set K = subrelstr ck;

A82: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;

A83: subrelstr ck is meet-inheriting

proof

subrelstr ck is join-inheriting
let x, y be Element of L; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of (subrelstr ck) or not y in the carrier of (subrelstr ck) or not ex_inf_of {x,y},L or "/\" ({x,y},L) in the carrier of (subrelstr ck) )

assume that

A84: x in the carrier of (subrelstr ck) and

A85: y in the carrier of (subrelstr ck) and

ex_inf_of {x,y},L ; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

end;assume that

A84: x in the carrier of (subrelstr ck) and

A85: y in the carrier of (subrelstr ck) and

ex_inf_of {x,y},L ; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

per cases
( ( x = a & y = a ) or ( x = a & y = b ) or ( x = a & y = c ) or ( x = a & y = d ) or ( x = a & y = e ) or ( x = b & y = a ) or ( x = b & y = b ) or ( x = b & y = c ) or ( x = b & y = d ) or ( x = b & y = e ) or ( x = c & y = a ) or ( x = c & y = b ) or ( x = c & y = c ) or ( x = c & y = d ) or ( x = c & y = e ) or ( x = d & y = a ) or ( x = d & y = b ) or ( x = d & y = c ) or ( x = d & y = d ) or ( x = d & y = e ) or ( x = e & y = a ) or ( x = e & y = b ) or ( x = e & y = c ) or ( x = e & y = d ) or ( x = e & y = e ) )
by A82, A84, A85, ENUMSET1:def 3;

end;

suppose
( x = a & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" a
by YELLOW_0:40;

then inf {x,y} = a by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = a by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" b
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A70, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A70, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A71, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A71, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A72, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A72, A82, ENUMSET1:def 3; :: thesis: verum

suppose A86:
( x = a & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A87:
c <= e
by A74, YELLOW_0:25;

a <= c by A71, YELLOW_0:25;

then a <= e by A87, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A86, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A71, YELLOW_0:25;

then a <= e by A87, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A86, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" b
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A70, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A70, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" b
by YELLOW_0:40;

then inf {x,y} = b by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = b by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A76, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A76, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A77, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A77, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A73, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A73, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A71, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A71, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A76, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A76, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" c
by YELLOW_0:40;

then inf {x,y} = c by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = c by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A78, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A78, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A74, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A74, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A72, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A72, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A77, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A77, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A78, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A78, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = d "/\" d
by YELLOW_0:40;

then inf {x,y} = d by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = d by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = d "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A75, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A75, A82, ENUMSET1:def 3; :: thesis: verum

suppose A88:
( x = e & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A89:
c <= e
by A74, YELLOW_0:25;

a <= c by A71, YELLOW_0:25;

then a <= e by A89, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A88, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A71, YELLOW_0:25;

then a <= e by A89, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A88, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = e & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A73, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A73, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = e & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A74, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A74, A82, ENUMSET1:def 3; :: thesis: verum

proof

then reconsider K = subrelstr ck as non empty full Sublattice of L by A83, YELLOW_0:def 15;
let x, y be Element of L; :: according to YELLOW_0:def 17 :: thesis: ( not x in the carrier of (subrelstr ck) or not y in the carrier of (subrelstr ck) or not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of (subrelstr ck) )

assume that

A90: x in the carrier of (subrelstr ck) and

A91: y in the carrier of (subrelstr ck) and

ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

end;assume that

A90: x in the carrier of (subrelstr ck) and

A91: y in the carrier of (subrelstr ck) and

ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

per cases
( ( x = a & y = a ) or ( x = a & y = b ) or ( x = a & y = c ) or ( x = a & y = d ) or ( x = a & y = e ) or ( x = b & y = a ) or ( x = b & y = b ) or ( x = b & y = c ) or ( x = b & y = d ) or ( x = b & y = e ) or ( x = c & y = a ) or ( x = c & y = b ) or ( x = c & y = c ) or ( x = c & y = d ) or ( x = c & y = e ) or ( x = d & y = a ) or ( x = d & y = b ) or ( x = d & y = c ) or ( x = d & y = d ) or ( x = d & y = e ) or ( x = e & y = a ) or ( x = e & y = b ) or ( x = e & y = c ) or ( x = e & y = d ) or ( x = e & y = e ) )
by A82, A90, A91, ENUMSET1:def 3;

end;

suppose
( x = a & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = a "\/" a
by YELLOW_0:41;

then sup {x,y} = a by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = a by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
x "\/" y = b
by A70, Th5;

then sup {x,y} = b by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = b by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
x "\/" y = c
by A71, Th5;

then sup {x,y} = c by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = c by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
x "\/" y = d
by A72, Th5;

then sup {x,y} = d by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = d by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A92:
( x = a & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A93:
c <= e
by A74, YELLOW_0:25;

a <= c by A71, YELLOW_0:25;

then a <= e by A93, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A92, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A71, YELLOW_0:25;

then a <= e by A93, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A92, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A94:
( x = b & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

a "\/" b = b
by A70, Th5;

then sup {x,y} = b by A94, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = b by A94, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" b
by YELLOW_0:41;

then sup {x,y} = b by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = b by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" c
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A79, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A79, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" d
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A80, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A80, A82, ENUMSET1:def 3; :: thesis: verum

suppose A95:
( x = b & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

b "\/" e = e
by A73, Th5;

then sup {x,y} = e by A95, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A95, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A96:
( x = c & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

c "\/" a = c
by A71, Th5;

then sup {x,y} = c by A96, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = c by A96, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" c
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A79, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A79, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = c "\/" c
by YELLOW_0:41;

then sup {x,y} = c by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = c by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = c "\/" d
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A81, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A81, A82, ENUMSET1:def 3; :: thesis: verum

suppose A97:
( x = c & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

c "\/" e = e
by A74, Th5;

then sup {x,y} = e by A97, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A97, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
x "\/" y = d
by A72, Th5;

then sup {x,y} = d by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = d by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" d
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A80, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A80, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = c "\/" d
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A81, A82, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A81, A82, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = d "\/" d
by YELLOW_0:41;

then sup {x,y} = d by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = d by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A98:
( x = d & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

d "\/" e = e
by A75, Th5;

then sup {x,y} = e by A98, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A98, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A99:
( x = e & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A100:
c <= e
by A74, YELLOW_0:25;

a <= c by A71, YELLOW_0:25;

then a <= e by A100, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A99, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A71, YELLOW_0:25;

then a <= e by A100, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A99, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A101:
( x = e & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

b "\/" e = e
by A73, Th5;

then sup {x,y} = e by A101, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A101, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

suppose A102:
( x = e & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

c "\/" e = e
by A74, Th5;

then sup {x,y} = e by A102, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A102, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis: verum

take K ; :: thesis: M_3 ,K are_isomorphic

thus M_3 ,K are_isomorphic :: thesis: verum

proof

reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider dj = 2 \ 1 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;

defpred S_{1}[ object , object ] means for X being Element of M_3 st X = $1 holds

( ( X = z implies $2 = a ) & ( X = j implies $2 = b ) & ( X = dj implies $2 = c ) & ( X = td implies $2 = d ) & ( X = t implies $2 = e ) );

ex y being object st

( y in ck & S_{1}[x,y] )

A121: for x being object st x in the carrier of M_3 holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A114);

reconsider f = f as Function of M_3,K by A82;

ck c= rng f

A155: for x, y being Element of M_3 holds

( x <= y iff f . x <= f . y )

f is V13() by A122;

hence f is isomorphic by A82, A154, A155, WAYBEL_0:66; :: thesis: verum

end;reconsider td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;

reconsider dj = 2 \ 1 as Element of M_3 by A1, ENUMSET1:def 3;

A104: now :: thesis: not dj = t

A105:
2 in t
by CARD_1:51, ENUMSET1:def 1;

assume dj = t ; :: thesis: contradiction

hence contradiction by A105, Th2, TARSKI:def 1; :: thesis: verum

end;assume dj = t ; :: thesis: contradiction

hence contradiction by A105, Th2, TARSKI:def 1; :: thesis: verum

A106: now :: thesis: not td = t

reconsider j = 1 as Element of M_3 by A1, ENUMSET1:def 3;A107:
0 in t
by CARD_1:51, ENUMSET1:def 1;

assume td = t ; :: thesis: contradiction

hence contradiction by A107, Th4, TARSKI:def 1; :: thesis: verum

end;assume td = t ; :: thesis: contradiction

hence contradiction by A107, Th4, TARSKI:def 1; :: thesis: verum

reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;

defpred S

( ( X = z implies $2 = a ) & ( X = j implies $2 = b ) & ( X = dj implies $2 = c ) & ( X = td implies $2 = d ) & ( X = t implies $2 = e ) );

A108: now :: thesis: not j = dj

assume A109:
j = dj
; :: thesis: contradiction

1 in dj by Th2, TARSKI:def 1;

hence contradiction by A109; :: thesis: verum

end;1 in dj by Th2, TARSKI:def 1;

hence contradiction by A109; :: thesis: verum

A110: now :: thesis: not j = td

assume A111:
j = td
; :: thesis: contradiction

2 in td by Th4, TARSKI:def 1;

hence contradiction by A111, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;2 in td by Th4, TARSKI:def 1;

hence contradiction by A111, CARD_1:49, TARSKI:def 1; :: thesis: verum

A112: now :: thesis: not dj = td

A114:
for x being object st x in the carrier of M_3 holds assume A113:
dj = td
; :: thesis: contradiction

2 in td by Th4, TARSKI:def 1;

hence contradiction by A113, Th2, TARSKI:def 1; :: thesis: verum

end;2 in td by Th4, TARSKI:def 1;

hence contradiction by A113, Th2, TARSKI:def 1; :: thesis: verum

ex y being object st

( y in ck & S

proof

consider f being Function of the carrier of M_3,ck such that
let x be object ; :: thesis: ( x in the carrier of M_3 implies ex y being object st

( y in ck & S_{1}[x,y] ) )

assume A115: x in the carrier of M_3 ; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

end;( y in ck & S

assume A115: x in the carrier of M_3 ; :: thesis: ex y being object st

( y in ck & S

per cases
( x = 0 or x = 1 or x = 2 \ 1 or x = 3 \ 2 or x = 3 )
by A1, A115, ENUMSET1:def 3;

end;

suppose A116:
x = 0
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = a; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A116, Th2, Th4; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A116, Th2, Th4; :: thesis: verum

suppose A117:
x = 1
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = b; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A108, A110, A117; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A108, A110, A117; :: thesis: verum

suppose A118:
x = 2 \ 1
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = c; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A108, A112, A104, A118, Th2; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A108, A112, A104, A118, Th2; :: thesis: verum

suppose A119:
x = 3 \ 2
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = d; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A110, A112, A106, A119, Th4; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A110, A112, A106, A119, Th4; :: thesis: verum

suppose A120:
x = 3
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = e; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A104, A106, A120; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of M_3; :: thesis: ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A104, A106, A120; :: thesis: verum

A121: for x being object st x in the carrier of M_3 holds

S

reconsider f = f as Function of M_3,K by A82;

A122: now :: thesis: for x, y being Element of M_3 st f . x = f . y holds

x = y

A144:
rng f c= ck
x = y

let x, y be Element of M_3; :: thesis: ( f . x = f . y implies x = y )

assume A123: f . x = f . y ; :: thesis: x = y

thus x = y :: thesis: verum

end;assume A123: f . x = f . y ; :: thesis: x = y

thus x = y :: thesis: verum

proof
end;

per cases
( ( x = z & y = z ) or ( x = j & y = j ) or ( x = dj & y = dj ) or ( x = td & y = td ) or ( x = t & y = t ) or ( x = z & y = j ) or ( x = z & y = dj ) or ( x = z & y = td ) or ( x = z & y = t ) or ( x = j & y = z ) or ( x = j & y = dj ) or ( x = j & y = td ) or ( x = j & y = t ) or ( x = dj & y = z ) or ( x = dj & y = j ) or ( x = dj & y = td ) or ( x = dj & y = t ) or ( x = td & y = z ) or ( x = td & y = j ) or ( x = td & y = dj ) or ( x = td & y = t ) or ( x = t & y = z ) or ( x = t & y = j ) or ( x = t & y = dj ) or ( x = t & y = td ) )
by A1, ENUMSET1:def 3;

end;

proof

A147:
dom f = the carrier of M_3
by FUNCT_2:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in ck )

assume y in rng f ; :: thesis: y in ck

then consider x being object such that

A145: x in dom f and

A146: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of M_3 by A145;

( x = z or x = j or x = dj or x = td or x = t ) by A1, ENUMSET1:def 3;

then ( y = a or y = d or y = c or y = b or y = e ) by A121, A146;

hence y in ck by ENUMSET1:def 3; :: thesis: verum

end;assume y in rng f ; :: thesis: y in ck

then consider x being object such that

A145: x in dom f and

A146: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of M_3 by A145;

( x = z or x = j or x = dj or x = td or x = t ) by A1, ENUMSET1:def 3;

then ( y = a or y = d or y = c or y = b or y = e ) by A121, A146;

hence y in ck by ENUMSET1:def 3; :: thesis: verum

ck c= rng f

proof

then A154:
rng f = ck
by A144;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ck or y in rng f )

assume A148: y in ck ; :: thesis: y in rng f

end;assume A148: y in ck ; :: thesis: y in rng f

A155: for x, y being Element of M_3 holds

( x <= y iff f . x <= f . y )

proof

take
f
; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
let x, y be Element of M_3; :: thesis: ( x <= y iff f . x <= f . y )

thus ( x <= y implies f . x <= f . y ) :: thesis: ( f . x <= f . y implies x <= y )

end;thus ( x <= y implies f . x <= f . y ) :: thesis: ( f . x <= f . y implies x <= y )

proof

thus
( f . x <= f . y implies x <= y )
:: thesis: verum
assume A156:
x <= y
; :: thesis: f . x <= f . y

end;per cases
( ( x = z & y = z ) or ( x = z & y = j ) or ( x = z & y = dj ) or ( x = z & y = td ) or ( x = z & y = t ) or ( x = j & y = z ) or ( x = j & y = j ) or ( x = j & y = dj ) or ( x = j & y = td ) or ( x = j & y = t ) or ( x = dj & y = z ) or ( x = dj & y = j ) or ( x = dj & y = dj ) or ( x = dj & y = td ) or ( x = dj & y = t ) or ( x = td & y = z ) or ( x = td & y = j ) or ( x = td & y = dj ) or ( x = td & y = td ) or ( x = td & y = t ) or ( x = t & y = z ) or ( x = t & y = j ) or ( x = t & y = dj ) or ( x = t & y = td ) or ( x = t & y = t ) )
by A1, ENUMSET1:def 3;

end;

suppose A157:
( x = z & y = j )
; :: thesis: f . x <= f . y

then A158:
f . y = b
by A121;

A159: a <= b by A70, YELLOW_0:25;

f . x = a by A121, A157;

hence f . x <= f . y by A158, A159, YELLOW_0:60; :: thesis: verum

end;A159: a <= b by A70, YELLOW_0:25;

f . x = a by A121, A157;

hence f . x <= f . y by A158, A159, YELLOW_0:60; :: thesis: verum

suppose A160:
( x = z & y = dj )
; :: thesis: f . x <= f . y

then A161:
f . y = c
by A121;

A162: a <= c by A71, YELLOW_0:25;

f . x = a by A121, A160;

hence f . x <= f . y by A161, A162, YELLOW_0:60; :: thesis: verum

end;A162: a <= c by A71, YELLOW_0:25;

f . x = a by A121, A160;

hence f . x <= f . y by A161, A162, YELLOW_0:60; :: thesis: verum

suppose A163:
( x = z & y = td )
; :: thesis: f . x <= f . y

then A164:
f . y = d
by A121;

A165: a <= d by A72, YELLOW_0:25;

f . x = a by A121, A163;

hence f . x <= f . y by A164, A165, YELLOW_0:60; :: thesis: verum

end;A165: a <= d by A72, YELLOW_0:25;

f . x = a by A121, A163;

hence f . x <= f . y by A164, A165, YELLOW_0:60; :: thesis: verum

suppose A166:
( x = z & y = t )
; :: thesis: f . x <= f . y

A167:
c <= e
by A74, YELLOW_0:25;

a <= c by A71, YELLOW_0:25;

then A168: a <= e by A167, ORDERS_2:3;

A169: f . y = e by A121, A166;

f . x = a by A121, A166;

hence f . x <= f . y by A169, A168, YELLOW_0:60; :: thesis: verum

end;a <= c by A71, YELLOW_0:25;

then A168: a <= e by A167, ORDERS_2:3;

A169: f . y = e by A121, A166;

f . x = a by A121, A166;

hence f . x <= f . y by A169, A168, YELLOW_0:60; :: thesis: verum

suppose A170:
( x = j & y = dj )
; :: thesis: f . x <= f . y

0 in j
by CARD_1:49, TARSKI:def 1;

then not j c= dj by Th2, TARSKI:def 1;

hence f . x <= f . y by A156, A170, YELLOW_1:3; :: thesis: verum

end;then not j c= dj by Th2, TARSKI:def 1;

hence f . x <= f . y by A156, A170, YELLOW_1:3; :: thesis: verum

suppose A171:
( x = j & y = td )
; :: thesis: f . x <= f . y

0 in j
by CARD_1:49, TARSKI:def 1;

then not j c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A156, A171, YELLOW_1:3; :: thesis: verum

end;then not j c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A156, A171, YELLOW_1:3; :: thesis: verum

suppose A172:
( x = j & y = t )
; :: thesis: f . x <= f . y

then A173:
f . y = e
by A121;

A174: b <= e by A73, YELLOW_0:25;

f . x = b by A121, A172;

hence f . x <= f . y by A173, A174, YELLOW_0:60; :: thesis: verum

end;A174: b <= e by A73, YELLOW_0:25;

f . x = b by A121, A172;

hence f . x <= f . y by A173, A174, YELLOW_0:60; :: thesis: verum

suppose A175:
( x = dj & y = j )
; :: thesis: f . x <= f . y

A176:
not 1 in j
;

1 in dj by Th2, TARSKI:def 1;

then not dj c= j by A176;

hence f . x <= f . y by A156, A175, YELLOW_1:3; :: thesis: verum

end;1 in dj by Th2, TARSKI:def 1;

then not dj c= j by A176;

hence f . x <= f . y by A156, A175, YELLOW_1:3; :: thesis: verum

suppose A177:
( x = dj & y = td )
; :: thesis: f . x <= f . y

1 in dj
by Th2, TARSKI:def 1;

then not dj c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A156, A177, YELLOW_1:3; :: thesis: verum

end;then not dj c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A156, A177, YELLOW_1:3; :: thesis: verum

suppose A178:
( x = dj & y = t )
; :: thesis: f . x <= f . y

then A179:
f . y = e
by A121;

A180: c <= e by A74, YELLOW_0:25;

f . x = c by A121, A178;

hence f . x <= f . y by A179, A180, YELLOW_0:60; :: thesis: verum

end;A180: c <= e by A74, YELLOW_0:25;

f . x = c by A121, A178;

hence f . x <= f . y by A179, A180, YELLOW_0:60; :: thesis: verum

suppose A181:
( x = td & y = j )
; :: thesis: f . x <= f . y

2 in td
by Th4, TARSKI:def 1;

then not td c= j by CARD_1:49, TARSKI:def 1;

hence f . x <= f . y by A156, A181, YELLOW_1:3; :: thesis: verum

end;then not td c= j by CARD_1:49, TARSKI:def 1;

hence f . x <= f . y by A156, A181, YELLOW_1:3; :: thesis: verum

suppose A182:
( x = td & y = dj )
; :: thesis: f . x <= f . y

2 in td
by Th4, TARSKI:def 1;

then not td c= dj by Th2, TARSKI:def 1;

hence f . x <= f . y by A156, A182, YELLOW_1:3; :: thesis: verum

end;then not td c= dj by Th2, TARSKI:def 1;

hence f . x <= f . y by A156, A182, YELLOW_1:3; :: thesis: verum

suppose A183:
( x = td & y = t )
; :: thesis: f . x <= f . y

then A184:
f . y = e
by A121;

A185: d <= e by A75, YELLOW_0:25;

f . x = d by A121, A183;

hence f . x <= f . y by A184, A185, YELLOW_0:60; :: thesis: verum

end;A185: d <= e by A75, YELLOW_0:25;

f . x = d by A121, A183;

hence f . x <= f . y by A184, A185, YELLOW_0:60; :: thesis: verum

suppose A186:
( x = t & y = j )
; :: thesis: f . x <= f . y

A187:
not 1 in j
;

1 in t by CARD_1:51, ENUMSET1:def 1;

then not t c= j by A187;

hence f . x <= f . y by A156, A186, YELLOW_1:3; :: thesis: verum

end;1 in t by CARD_1:51, ENUMSET1:def 1;

then not t c= j by A187;

hence f . x <= f . y by A156, A186, YELLOW_1:3; :: thesis: verum

suppose A188:
( x = t & y = dj )
; :: thesis: f . x <= f . y

2 in t
by CARD_1:51, ENUMSET1:def 1;

then not t c= dj by Th2, TARSKI:def 1;

hence f . x <= f . y by A156, A188, YELLOW_1:3; :: thesis: verum

end;then not t c= dj by Th2, TARSKI:def 1;

hence f . x <= f . y by A156, A188, YELLOW_1:3; :: thesis: verum

suppose A189:
( x = t & y = td )
; :: thesis: f . x <= f . y

0 in t
by CARD_1:51, ENUMSET1:def 1;

then not t c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A156, A189, YELLOW_1:3; :: thesis: verum

end;then not t c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A156, A189, YELLOW_1:3; :: thesis: verum

proof

A190:
dj c= t

A192: f . x in ck by A147, A154, FUNCT_1:def 3;

assume A193: f . x <= f . y ; :: thesis: x <= y

end;proof

A191:
f . y in ck
by A147, A154, FUNCT_1:def 3;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in dj or X in t )

assume X in dj ; :: thesis: X in t

then X = 1 by Th2, TARSKI:def 1;

hence X in t by CARD_1:51, ENUMSET1:def 1; :: thesis: verum

end;assume X in dj ; :: thesis: X in t

then X = 1 by Th2, TARSKI:def 1;

hence X in t by CARD_1:51, ENUMSET1:def 1; :: thesis: verum

A192: f . x in ck by A147, A154, FUNCT_1:def 3;

assume A193: f . x <= f . y ; :: thesis: x <= y

per cases
( ( f . x = a & f . y = a ) or ( f . x = a & f . y = b ) or ( f . x = a & f . y = c ) or ( f . x = a & f . y = d ) or ( f . x = a & f . y = e ) or ( f . x = b & f . y = a ) or ( f . x = b & f . y = b ) or ( f . x = b & f . y = c ) or ( f . x = b & f . y = d ) or ( f . x = b & f . y = e ) or ( f . x = c & f . y = a ) or ( f . x = c & f . y = b ) or ( f . x = c & f . y = c ) or ( f . x = c & f . y = d ) or ( f . x = c & f . y = e ) or ( f . x = d & f . y = a ) or ( f . x = d & f . y = b ) or ( f . x = d & f . y = c ) or ( f . x = d & f . y = d ) or ( f . x = d & f . y = e ) or ( f . x = e & f . y = a ) or ( f . x = e & f . y = b ) or ( f . x = e & f . y = c ) or ( f . x = e & f . y = d ) or ( f . x = e & f . y = e ) )
by A192, A191, ENUMSET1:def 3;

end;

suppose A194:
( f . x = a & f . y = b )
; :: thesis: x <= y

f . z = a
by A121;

then z = x by A122, A194;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A122, A194;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

suppose A195:
( f . x = a & f . y = c )
; :: thesis: x <= y

f . z = a
by A121;

then z = x by A122, A195;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A122, A195;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

suppose A196:
( f . x = a & f . y = d )
; :: thesis: x <= y

f . z = a
by A121;

then z = x by A122, A196;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A122, A196;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

suppose A197:
( f . x = a & f . y = e )
; :: thesis: x <= y

f . z = a
by A121;

then z = x by A122, A197;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A122, A197;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

suppose A198:
( f . x = b & f . y = e )
; :: thesis: x <= y

f . t = e
by A121;

then A199: t = y by A122, A198;

f . j = b by A121;

then A200: j = x by A122, A198;

Segm 1 c= Segm 3 by NAT_1:39;

hence x <= y by YELLOW_1:3, A200, A199; :: thesis: verum

end;then A199: t = y by A122, A198;

f . j = b by A121;

then A200: j = x by A122, A198;

Segm 1 c= Segm 3 by NAT_1:39;

hence x <= y by YELLOW_1:3, A200, A199; :: thesis: verum

suppose A201:
( f . x = c & f . y = e )
; :: thesis: x <= y

f . t = e
by A121;

then A202: t = y by A122, A201;

f . dj = c by A121;

then dj = x by A122, A201;

hence x <= y by A190, A202, YELLOW_1:3; :: thesis: verum

end;then A202: t = y by A122, A201;

f . dj = c by A121;

then dj = x by A122, A201;

hence x <= y by A190, A202, YELLOW_1:3; :: thesis: verum

suppose A203:
( f . x = d & f . y = e )
; :: thesis: x <= y

f . t = e
by A121;

then A204: t = y by A122, A203;

f . td = d by A121;

then td = x by A122, A203;

hence x <= y by A204, YELLOW_1:3; :: thesis: verum

end;then A204: t = y by A122, A203;

f . td = d by A121;

then td = x by A122, A203;

hence x <= y by A204, YELLOW_1:3; :: thesis: verum

suppose A205:
( f . x = e & f . y = a )
; :: thesis: x <= y

A206:
a <= b
by A70, YELLOW_0:25;

e <= a by A193, A205, YELLOW_0:59;

then e <= b by A206, ORDERS_2:3;

hence x <= y by AAA, A73, YELLOW_0:25; :: thesis: verum

end;e <= a by A193, A205, YELLOW_0:59;

then e <= b by A206, ORDERS_2:3;

hence x <= y by AAA, A73, YELLOW_0:25; :: thesis: verum

f is V13() by A122;

hence f is isomorphic by A82, A154, A155, WAYBEL_0:66; :: thesis: verum