let p, q be Point of (); :: thesis: for f being Function of (),() st f = Sq_Circ & p in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & q in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) holds
(f . p) `1 <= (f . q) `1

let f be Function of (),(); :: thesis: ( f = Sq_Circ & p in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & q in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) implies (f . p) `1 <= (f . q) `1 )
assume that
A1: f = Sq_Circ and
A2: p in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) and
A3: q in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: (f . p) `1 <= (f . q) `1
A4: p `1 = - 1 by ;
A5: - 1 <= p `2 by ;
A6: p `2 <= 1 by ;
A7: q `2 = - 1 by ;
A8: - 1 <= q `1 by ;
A9: q `1 <= 1 by ;
A10: p <> 0. () by ;
A11: q <> 0. () by ;
p `2 <= - (p `1) by A2, A4, Th1;
then f . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by ;
then A12: (f . p) `1 = (- 1) / (sqrt (1 + (((p `2) / (- 1)) ^2))) by
.= (- 1) / (sqrt (1 + ((p `2) ^2))) ;
(p `2) ^2 >= 0 by XREAL_1:63;
then A13: sqrt (1 + ((p `2) ^2)) > 0 by SQUARE_1:25;
(q `1) ^2 >= 0 by XREAL_1:63;
then A14: sqrt (1 + ((q `1) ^2)) > 0 by SQUARE_1:25;
q `1 <= - (q `2) by A3, A7, Th3;
then f . q = |[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]| by ;
then A15: (f . q) `1 = (q `1) / (sqrt (1 + (((q `1) / (- 1)) ^2))) by
.= (q `1) / (sqrt (1 + ((q `1) ^2))) ;
- (sqrt (1 + ((q `1) ^2))) <= (q `1) * (sqrt (1 + ((p `2) ^2))) by ;
then ((- 1) * (sqrt (1 + ((q `1) ^2)))) / (sqrt (1 + ((q `1) ^2))) <= ((q `1) * (sqrt (1 + ((p `2) ^2)))) / (sqrt (1 + ((q `1) ^2))) by ;
then - 1 <= ((q `1) * (sqrt (1 + ((p `2) ^2)))) / (sqrt (1 + ((q `1) ^2))) by ;
then - 1 <= ((q `1) / (sqrt (1 + ((q `1) ^2)))) * (sqrt (1 + ((p `2) ^2))) by XCMPLX_1:74;
then (- 1) / (sqrt (1 + ((p `2) ^2))) <= (((q `1) / (sqrt (1 + ((q `1) ^2)))) * (sqrt (1 + ((p `2) ^2)))) / (sqrt (1 + ((p `2) ^2))) by ;
hence (f . p) `1 <= (f . q) `1 by ; :: thesis: verum